From 879e5c4aa7687be63527845ba34d2d0bb12546a3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Dec 2005 15:05:21 +0000
Subject: [PATCH] eval_from_stream_greedy finally got rid of!

---
 helm/matita/matitaEngine.ml  | 36 ++++++++++++------------------------
 helm/matita/matitaEngine.mli |  9 +--------
 helm/matita/matitacLib.ml    | 13 +++++++------
 3 files changed, 20 insertions(+), 38 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index cfbf74798..457f376bb 100644
--- 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 b97361979..8c469df39 100644
--- 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 b2c3e9a32..355ceed60 100644
--- 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 = 
-- 
2.39.2