eval_from_stream_greedy finally got rid of!

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index cfbf74798d8ef661ee13395cd13e7153bfb2107f..457f376bb2c0afcb3b3540a68aeaca84f482d94e 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,43 +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
-        ~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
-    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
-      ~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 
+     eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast
   done
 ;;
 
 let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
+ try
   eval_from_stream 
     ?do_heavy_checks ~include_paths ?clean_baseuri status
       (Ulexing.from_utf8_string str) (fun _ _ -> ())
+ with End_of_file -> ()
 
 let default_options () = no_options