From f6a4599b852a32351163eb272d14718e32b58cec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Jul 2017 13:12:03 +0200
Subject: A less intrusive Profile.close_profile.

No need to call Gc functions nor Unix timing functions when there is
nothing to report.

Moreover, PMP observed problems with these functions in the
debugger. PMP also reported that Gc.minor takes some noticeable time,
so no need to trigger some when unneeded.
---
 lib/profile.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index b669161858..78bf35621a 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -317,15 +317,15 @@ let adjust_time ov_bc ov_ad e =
      owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
 
 let close_profile print =
-  let dw = spent_alloc () in
-  let t = get_time () in
-  match !stack with
-    | [outside] ->
-	outside.tottime <- outside.tottime + t;
-	outside.owntime <- outside.owntime + t;
-	ajoute_ownalloc outside dw;
-	ajoute_totalloc outside dw;
-	if !prof_table <> [] then begin
+  if !prof_table <> [] then begin
+      let dw = spent_alloc () in
+      let t = get_time () in
+      match !stack with
+      | [outside] ->
+	  outside.tottime <- outside.tottime + t;
+	  outside.owntime <- outside.owntime + t;
+	  ajoute_ownalloc outside dw;
+	  ajoute_totalloc outside dw;
 	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
 	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
 	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
@@ -346,8 +346,8 @@ let close_profile print =
 	  in
 	  if print then format_profile updated_data;
 	  init_profile ()
-	end
-    | _ -> failwith "Inconsistency"
+      | _ -> failwith "Inconsistency"
+    end
 
 let print_profile () = close_profile true
 
-- 
cgit v1.2.3