added chronometer

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 607fe703b065c1f122b0c17309c5cad997776736..ef0ab5a99ccf6fcbb170294ad0b0343e9add02a4 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
@@ -85,8 +84,22 @@ let run_script fname =
         
 let _ = 
   List.iter (fun fname -> 
+    let time = Unix.time () in
+    MatitaLog.message (sprintf "execution of %s started:" fname);
     run_script fname;
-    MatitaLog.message (sprintf "execution of %s completed." fname)) scripts;
+    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
+    MatitaLog.message 
+      (sprintf "execution of %s completed in %s." fname (hou^min^sec))) scripts;
   Http_getter.sync_dump_file ();
   exit(0)