X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=dcb0baebf155699fd7fbddc02e4c7b8110fc717b;hb=f3ae21edf39f33e4e9af1fafa1d2cde119d5cdc6;hp=c58e0fa3928a4dd05dc7efa9d9d445da6e9086eb;hpb=675c9cf70d8537d70675b5520ca708fe75c67aed;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c58e0fa39..dcb0baebf 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -180,7 +180,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = let title = "Unable to include " ^ what in let message = what ^ " is not handled by a development.\n" ^ - "All dependencies are authomatically solved for a development.\n\n" ^ + "All dependencies are automatically solved for a development.\n\n" ^ "Do you want to set up a development?" in (match guistuff.ask_confirmation ~title ~message with @@ -232,7 +232,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = let l = MQ.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." - (MatitaMisc.trim_blanks unparsed_text) + (HExtlib.trim_blanks unparsed_text) in let entry = `Whelp (query_url, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; @@ -583,7 +583,7 @@ object (self) List.iter (fun o -> o status) observers method loadFromFile f = - buffer#set_text (MatitaMisc.input_file f); + buffer#set_text (HExtlib.input_file f); self#reset_buffer; buffer#set_modified false @@ -629,7 +629,7 @@ object (self) buffer#set_modified false method template () = - let template = MatitaMisc.input_file BuildTimeConf.script_template in + let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; guistuff.filenamedata <- (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));