From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 11:59:55 +0000 (+0000)
Subject: Use eval_from_stream in place of eval_from_stream_ref to avoid printing the
X-Git-Tag: PRE_GETTER_STORAGE~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fe9fe9574ea2383032cbb0115ac18853a31972d2;p=helm.git

Use eval_from_stream in place of eval_from_stream_ref to avoid printing the
prompt.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 17532cc90..5e3e33606 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -220,7 +220,7 @@ let generate_projections uri fields status =
   ) status projections
 
 (* to avoid a long list of recursive functions *)
-let eval_from_stream_greedy_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
  
 let eval_command status cmd =
   match cmd with
@@ -228,14 +228,7 @@ let eval_command status cmd =
      let path = MatitaMisc.obj_file_of_script path in
      let stream = Stream.of_channel (open_in path) in
      let status = ref status in
-      (try
-        !eval_from_stream_greedy_ref status stream (fun _ _ -> ())
-       with
-         CicTextualParser2.Parse_error (floc,err) as exc ->
-          (* check for EOI *)
-          if Stream.peek stream = None then ()
-          else raise exc
-      );
+      !eval_from_stream_ref status stream (fun _ _ -> ());
       !status
   | TacticAst.Set (loc, name, value) -> 
       let value = 
@@ -586,7 +579,11 @@ let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
   List.iter
    (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+;;
 
+(* to avoid a long list of recursive functions *)
+eval_from_stream_ref := eval_from_stream;;
+  
 let eval_from_stream_greedy status str cb =
   while true do
     print_string "matita> ";
@@ -597,9 +594,6 @@ let eval_from_stream_greedy status str cb =
   done
 ;;
 
-(* to avoid a long list of recursive functions *)
-eval_from_stream_greedy_ref := eval_from_stream_greedy;;
-  
 let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())