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 17532cc90f21469a2816c158c6a88b59380ac34b..5e3e336060bb8c15b9ad8faecf0d56ad8bd114cb 100644 (file)
--- 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 _ _ -> ())