fixed matitac

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 4ca54d0e40dbd5d97b3df4596f77e56ff5b8fc76..f1b8f074c4dace915e1a51fefe3b94e9ab74e8d4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -505,12 +505,14 @@ let eval_ast status ast =
   (* this disambiguation step should be deferred to support tacticals *)
   eval status st
 
-let eval_from_stream status str =
-  let st = CicTextualParser2.parse_statement str in
-  eval_ast status st
+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
   
 let eval_string status str =
-  eval_from_stream status (Stream.of_string str) 
+  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
   let options =

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index 3fcc4cc3ee7f864180f20c79398ec0bb4b8b9512..d549405bbb6064c97db11300c916c6b00da36f4b 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -27,7 +27,10 @@
 
 val eval_string: MatitaTypes.status -> string -> MatitaTypes.status
 
-val eval_from_stream: MatitaTypes.status -> char Stream.t -> MatitaTypes.status
+val eval_from_stream: 
+  MatitaTypes.status -> char Stream.t -> 
+    (MatitaTypes.status -> (CicAst.term,string) TacticAst.statement -> unit) ->
+    MatitaTypes.status
 
 val eval_ast: 
   MatitaTypes.status -> (CicAst.term, string) TacticAst.statement ->

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 4dbac36539ac238afd0ddcc8f6e8a73d477211bf..607fe703b065c1f122b0c17309c5cad997776736 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -58,32 +58,36 @@ let run_script fname =
       | fname -> open_in fname)
   in
   let status = ref (Lazy.force MatitaEngine.initial_status) in
+  let slash_n_RE = Pcre.regexp "\\n" in
+  let cb status stm = 
+    (* dump_status status; *)
+    let stm = TacticAstPp.pp_statement stm in
+    let stm = Pcre.replace ~rex:slash_n_RE stm in
+    let stm = 
+      if String.length stm > 50 then
+        String.sub stm 0 50 ^ " ..."
+      else
+        stm
+    in
+    MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
+  in
   try
-    while true do
-      dump_status !status;
-      try
-        status := MatitaEngine.eval_from_stream !status is
-      with
-      | CicTextualParser2.Parse_error _ as exn -> 
-          try 
-            Stream.empty is; 
-            raise  End_of_file
-          with Stream.Failure -> raise exn
-      | exn -> 
-          MatitaLog.error (Printexc.to_string exn);
-          raise exn
-    done
-  with 
-    | End_of_file ->
-        MatitaLog.message (sprintf "execution of %s completed." fname);
-        Http_getter.sync_dump_file ();
-        exit(0)
-    | CicTextualParser2.Parse_error (floc,err) ->
-        let (x, y) = CicAst.loc_of_floc floc in
-        MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err);
-        Http_getter.sync_dump_file ();
-        exit 1
+    status := MatitaEngine.eval_from_stream !status is cb
+  with
+  | CicTextualParser2.Parse_error (floc,err) ->
+     let (x, y) = CicAst.loc_of_floc floc in
+     MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err);
+     Http_getter.sync_dump_file ();
+     exit 1
+  | exn -> 
+      MatitaLog.error (Printexc.to_string exn);
+      raise exn
         
-
-let _ = List.iter run_script scripts
+let _ = 
+  List.iter (fun fname -> 
+    run_script fname;
+    MatitaLog.message (sprintf "execution of %s completed." fname)) scripts;
+  Http_getter.sync_dump_file ();
+  exit(0)
+