From c72b0d76d607482bccf12e7193a4d1a777815b91 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Nov 2005 16:30:33 +0000 Subject: [PATCH] added calbback to make the profiler silent --- helm/ocaml/extlib/hExtlib.ml | 11 ++++++++--- helm/ocaml/extlib/hExtlib.mli | 1 + 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index c09dcf2c1..c66236e43 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -26,11 +26,15 @@ (** PROFILING *) +(* we should use a key in te registry, but we can't see the registry.. *) let profiling_enabled = true +let profiling_printings = ref (fun () -> true) +let set_profiling_printings f = profiling_printings := f + type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } let profile ?(enable = true) = - if profiling_enabled && enable then + if profiling_enabled && enable then function s -> let total = ref 0.0 in let profile f x = @@ -48,8 +52,9 @@ let profile ?(enable = true) = in at_exit (fun () -> - print_endline - ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); + if !profiling_printings () then + prerr_endline + ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); { profile = profile } else function _ -> { profile = fun f x -> f x } diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index 6e0484b87..d12c042f5 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -74,4 +74,5 @@ type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } (** @return a profiling function; [s] is used for labelling the total time at * the end of the execution *) val profile : ?enable:bool -> string -> profiler +val set_profiling_printings : (unit -> bool) -> unit -- 2.39.2