From fe9fe9574ea2383032cbb0115ac18853a31972d2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 11:59:55 +0000 Subject: [PATCH] Use eval_from_stream in place of eval_from_stream_ref to avoid printing the prompt. --- helm/matita/matitaEngine.ml | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) 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 _ _ -> ()) -- 2.39.2