From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Sep 2005 17:02:21 +0000 (+0000)
Subject: Profiling did not profile functions that raise an exception!
X-Git-Tag: LAST_BEFORE_NEW~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f6ce528977597b1745e97a1cb3778d3335b8133;p=helm.git

Profiling did not profile functions that raise an exception!
Fixed.
---

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 07f39896c..8bb137f20 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -209,7 +209,7 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
-let profiling_enabled = false
+let profiling_enabled = true
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile =
@@ -218,10 +218,16 @@ let profile =
    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
+    try
+     let res = f x in
+     let after = Unix.gettimeofday () in
+      total := !total +. (after -. before);
+      res
+    with
+     exc ->
+      let after = Unix.gettimeofday () in
+       total := !total +. (after -. before);
+       raise exc
    in
    at_exit
     (fun () ->