eval_from_stream_greedy finally got rid of!

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
 

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index b97361979fa9a0e420acb0e9266a990b22a3eabb..8c469df391458d2369f45621f9b624ba713041d7 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -32,6 +32,7 @@ val eval_string:
     GrafiteTypes.status ref -> string -> unit
 
 val eval_from_stream: 
+  ?prompt:bool ->
   ?do_heavy_checks:bool ->
   include_paths:string list ->
   ?clean_baseuri:bool ->
@@ -39,12 +40,4 @@ val eval_from_stream:
   (GrafiteTypes.status -> GrafiteParser.statement -> unit) ->
     unit
 
-val eval_from_stream_greedy: 
-  ?do_heavy_checks:bool ->
-  include_paths:string list ->
-  ?clean_baseuri:bool ->
-  GrafiteTypes.status ref-> Ulexing.lexbuf -> 
-  (GrafiteTypes.status -> GrafiteParser.statement -> unit) ->
-    unit
-
 val initial_status: GrafiteTypes.status lazy_t

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index b2c3e9a323070ca26c2c5c2aef159ce52d66ad8c..355ceed6044385e3e325ca9f73008b11ac26f37d 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -98,7 +98,7 @@ let rec interactive_loop () =
   let str = Ulexing.from_utf8_channel stdin in
   try
     run_script str 
-      (MatitaEngine.eval_from_stream_greedy
+      (MatitaEngine.eval_from_stream ~prompt:true
       ~include_paths:(Helm_registry.get_list Helm_registry.string
         "matita.includes"))
   with 
@@ -154,11 +154,12 @@ let main ~mode =
         | "stdin" -> stdin
         | fname -> open_in fname) in
     let include_paths =
-     Helm_registry.get_list Helm_registry.string "matita.includes"
-    in
-    run_script is 
-      (MatitaEngine.eval_from_stream ~include_paths
-        ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
+     Helm_registry.get_list Helm_registry.string "matita.includes" in
+    (try
+      run_script is 
+       (MatitaEngine.eval_from_stream ~include_paths
+         ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
+     with End_of_file -> ());
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
     let sec =