* new binary matitatop

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 02f13739d5c14548e6da69f01a3c2c48e306d3e4..95de73528cf8ba1b273002e395026d11c2935d59 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -2,6 +2,8 @@
 open Printf
 open MatitaTypes
 
+exception Drop;;
+
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
@@ -223,6 +225,7 @@ let generate_projections uri fields status =
 let eval_command status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> set_option status name value
+  | TacticAst.Drop loc -> raise Drop
   | TacticAst.Qed loc ->
       let uri, metasenv, bo, ty = 
         match status.proof_status with
@@ -525,7 +528,7 @@ let disambiguate_command status = function
   | TacticAst.Coercion (loc, term) ->
       let status, term = disambiguate_term status term in
       status, TacticAst.Coercion (loc,term)
-  | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
+  | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
       status, cmd
   | TacticAst.Alias _ as x -> status, x
   | TacticAst.Obj (loc,obj) ->
@@ -567,9 +570,16 @@ let eval_ast status ast =
 
 let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
-  List.fold_left 
-    (fun status ast -> cb status ast;eval_ast status ast) status 
-  stl
+  List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+
+let eval_from_stream_greedy status str cb =
+  while true do
+    print_string "matita> ";
+    flush stdout;
+    let ast = CicTextualParser2.parse_statement str in
+    cb !status ast;
+    status := eval_ast !status ast 
+  done
   
 let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())