X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=457f376bb2c0afcb3b3540a68aeaca84f482d94e;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=c0f74962da394fd73325f75e869f637f45321603;hpb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c0f74962d..457f376bb 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,41 +30,31 @@ open GrafiteTypes
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-let eval_from_stream 
-  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
-=
-  try
-    while true do
-      let ast = GrafiteParser.parse_statement str in
-      cb !status ast;
-      status :=
-       GrafiteEngine.eval_ast
-        ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-        ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-        ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
-    done
-  with End_of_file -> ()
+let eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri status ast =
+ GrafiteEngine.eval_ast
+  ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
+  ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+  ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+  ?do_heavy_checks ?clean_baseuri status ast
 
-let eval_from_stream_greedy 
-  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+let eval_from_stream ?(prompt=false) ?do_heavy_checks ~include_paths
+ ?clean_baseuri status str cb 
 =
   while true do
-    print_string "matita> ";
-    flush stdout;
+    if prompt then (print_string "matita> "; flush stdout);
     let ast = GrafiteParser.parse_statement str in
     cb !status ast;
     status :=
-     GrafiteEngine.eval_ast
-      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-      ?do_heavy_checks ?include_paths ?clean_baseuri !status ast 
+     eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast
   done
 ;;
 
-let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
+let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
+ try
   eval_from_stream 
-    ?do_heavy_checks ?include_paths ?clean_baseuri status
+    ?do_heavy_checks ~include_paths ?clean_baseuri status
       (Ulexing.from_utf8_string str) (fun _ _ -> ())
+ with End_of_file -> ()
 
 let default_options () = no_options