X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Flib%2Ftime.ml;h=a9e542664f6f79134a2ae233b5bc6ca70087029b;hb=c450fdfb1b02eb69e5e7ef25f0acdf80157710df;hp=42d7d39a7be4abe740328657978bdf13821b28bb;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/lib/time.ml b/helm/software/helena/src/lib/time.ml
index 42d7d39a7..a9e542664 100644
--- a/helm/software/helena/src/lib/time.ml
+++ b/helm/software/helena/src/lib/time.ml
@@ -9,17 +9,17 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P = Printf
+module KP = Printf
+
 module L = Log
 
-let utime_stamp =
-   let old = ref 0.0 in
-   fun msg -> 
-      let times = Unix.times () in
-      let stamp = times.Unix.tms_utime in
-      let lap = stamp -. !old in
-      L.warn (P.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap);
-      old := stamp
+let level = 1 
+
+let old = [|0.0; 0.0|]
+
+let stamp_ix = 0
+
+let lap_ix = 1
 
 let gmtime msg =
    let gmt = Unix.gmtime (Unix.time ()) in
@@ -29,6 +29,27 @@ let gmtime msg =
    let h = gmt.Unix.tm_hour in
    let m = gmt.Unix.tm_min in
    let s = gmt.Unix.tm_sec in
-   L.warn (
-      P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s
-   )
+   let str = KP.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s in
+   L.warn level str
+
+let utime_stamp msg = 
+   let times = Unix.times () in
+   let stamp = times.Unix.tms_utime in
+   let lap = stamp -. old.(stamp_ix) in
+   let str = KP.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in
+   L.warn level str;
+   old.(stamp_ix) <- stamp
+
+IFDEF PROFV THEN
+
+let utime_lap msg = 
+   let times = Unix.times () in
+   let stamp = times.Unix.tms_utime in
+   if msg <> "" then begin
+      let lap = stamp -. old.(lap_ix) in
+      let str = KP.sprintf "USR TIME LAP (%s): %f" msg lap in
+      L.warn level str
+   end;
+   old.(lap_ix) <- stamp
+
+END