From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 Sep 2005 16:33:46 +0000 (+0000)
Subject: Enabling/disabling profiling is now controlled by a boolean (and not by a
X-Git-Tag: V_0_1_2_1~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d4c0e3f1bd4b142c3187d5a4d51f0ea5745d90b;p=helm.git

Enabling/disabling profiling is now controlled by a boolean (and not by a
comment!!!)
---

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 7269e1f84..aa1ed1ba0 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -209,21 +209,26 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
+let profiling_enabled = false
+
 let profile =
- function s ->
-  let total = ref 0.0 in
-  let profile f x =
-   let before = Unix.gettimeofday () in
-   let res = f x in
-   let after = Unix.gettimeofday () in
-    total := !total +. (after -. before);
-    res
-  in
-  at_exit
-   (fun () ->
-     print_endline
-      ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
-  profile
+ if profiling_enabled then
+  function s ->
+   let total = ref 0.0 in
+   let profile f x =
+    let before = Unix.gettimeofday () in
+    let res = f x in
+    let after = Unix.gettimeofday () in
+     total := !total +. (after -. before);
+     res
+   in
+   at_exit
+    (fun () ->
+      print_endline
+       ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
+   profile
+ else
+  function _ -> fun f x -> f x
 
 let id_of_annterm =
   function
@@ -243,7 +248,3 @@ let id_of_annterm =
   | Cic.AMutCase (id,_,_,_,_,_)
   | Cic.AFix (id,_,_)
   | Cic.ACoFix (id,_,_) -> id
-
-  (** WARNING: COMMENT THIS TO ENABLE PROFILING **)
-let profile _ = let profile f x = f x in profile
-