* the auto AST now has the width

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

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 4dbac36539ac238afd0ddcc8f6e8a73d477211bf..e7cdef9f4afb898ac82d492b58dab4a03a108965 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -50,7 +50,6 @@ let scripts =
   List.rev !acc
 
 let run_script fname =
-  MatitaLog.message (sprintf "execution of %s started:" fname);
   let is =
     Stream.of_channel
       (match fname with
@@ -58,32 +57,69 @@ 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 ;
+    !status
+  with
+  | CicTextualParser2.Parse_error (floc,err) ->
+     let (x, y) = CicAst.loc_of_floc floc in
+     MatitaLog.error (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 _ = 
+  at_exit
+    (fun () ->
+       Http_getter_logger.log "Sync map tree to disk...";
+       Http_getter.sync_dump_file ();
+       print_endline "\nThanks for using Matita!\n");
+  Sys.catch_break true;
+  try
+   List.iter (fun fname -> 
+    let time = Unix.time () in
+    MatitaLog.message (sprintf "execution of %s started:" fname);
+    let status = run_script fname in
+    let elapsed = Unix.time () -. time in
+    let tm = Unix.gmtime elapsed in
+    let sec = 
+      if tm.Unix.tm_sec > 0 then  (string_of_int tm.Unix.tm_sec ^ "''") else "" 
+    in
+    let min = 
+      if tm.Unix.tm_min > 0 then  (string_of_int tm.Unix.tm_min ^ "' ") else "" 
+    in
+    let hou = 
+      if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" 
+    in
+    let proof_status = status.proof_status in
+    if proof_status <> MatitaTypes.No_proof then
+     begin
+      MatitaLog.error
+       "there are still incomplete proofs at the end of the script";
+      exit(-1)
+     end
+    else
+     begin
+      MatitaLog.message 
+       (sprintf "execution of %s completed in %s." fname (hou^min^sec)) ;
+      exit(0)
+     end
+   ) scripts
+  with Sys.Break ->
+   MatitaLog.error "user break!";
+   exit (-1)