allow to switch profiling on and off on the fly

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 3ee270e4e00b42fd0b012a512b11a92feef48c82..0d7254c8bd48cd34b8374e11f6c224d3620213a8 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref true ;; (* ComponentsConf.profiling *)
 
 let something_profiled = ref false
 
@@ -47,11 +47,12 @@ let set_profiling_printings f = profiling_printings := f
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile ?(enable = true) s =
- if profiling_enabled && enable then
+ if !profiling_enabled && enable then
    let total = ref 0.0 in
    let calls = ref 0 in
    let max = ref 0.0 in
    let profile f x =
+    if not !profiling_enabled then f x else
     let before = Unix.gettimeofday () in
     try
      incr calls;
@@ -444,7 +445,7 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ as exn -> 
+       with Unix.Unix_error _ -> 
                aux tl
    in
    try

diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 73450ae11c62f7d860dcc9dface21a796767e132..30a6f145f11e22b0ad371d728182971d80cb5892 100644 (file)
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -129,3 +129,5 @@ val estimate_size: 'a -> int
 val is_prefix_of: string -> string -> bool
 val chop_prefix: string -> string -> string
 val touch: string -> unit
+
+val profiling_enabled: bool ref