snapshot, notably:

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

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 64870249019b5e8e79ef29f062870bf5504d4584..3f394cdb1108e9dc70158ad99d51c66b714bccc0 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -84,7 +84,7 @@ let interpreter =
     ~disambiguator ~currentProof ~console ~dbd ()
 
 let run_script fname =
-  message (sprintf "execution of %s started." fname);
+  message (sprintf "execution of %s started:" fname);
   let script =
     let ic = open_in fname in
     let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in
@@ -92,7 +92,7 @@ let run_script fname =
     ast
   in
   let rec aux = function
-    | [] -> ()
+    | [] -> ()  (* script is over *)
     | DisambiguateTypes.Comment _ :: tl -> aux tl
     | DisambiguateTypes.Command ast :: tl ->
         let loc =
@@ -107,7 +107,8 @@ let run_script fname =
         else
           aux tl
   in
-  aux script
+  aux script;
+  message (sprintf "execution of %s completed." fname)
 
 let _ = List.iter run_script scripts