X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=4296db49b668acde2ee35efc2aa87e0fe9f2018c;hb=9d37f725a8c150d2a9e20b24495e0cfdc7969ee6;hp=93eabf2acdfa355b73d89da1da474c8dd3f2708b;hpb=9ec9bec67c97942a048fe930faa53472754457c9;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 93eabf2ac..4296db49b 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -37,9 +37,11 @@ let profile ?(enable = true) = if profiling_enabled && enable then function s -> let total = ref 0.0 in + let calls = ref 0 in let profile f x = let before = Unix.gettimeofday () in try + incr calls; let res = f x in let after = Unix.gettimeofday () in total := !total +. (after -. before); @@ -54,7 +56,7 @@ let profile ?(enable = true) = (fun () -> if !profiling_printings () && !total <> 0. then prerr_endline - ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); + ("!! TOTAL TIME SPENT IN " ^ s ^ " ("^string_of_int !calls^"): " ^ string_of_float !total)); { profile = profile } else function _ -> { profile = fun f x -> f x }