# HG changeset patch
# User wenzelm
# Date 1305485422 -7200
# Node ID cce39fdaad7b087cd593a9144f322b2fb349aec8
# Parent  128cc195ced37f50a2fb64c0bd5e82b0c07b77d7
only show relevant timing;

diff -r 128cc195ced3 -r cce39fdaad7b src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Sun May 15 20:38:08 2011 +0200
+++ b/src/Pure/General/timing.ML	Sun May 15 20:50:22 2011 +0200
@@ -72,12 +72,22 @@
   Time.toString cpu ^ "s cpu time, " ^
   Time.toString gc ^ "s GC time" handle Time.Time => "";
 
+val min_time = Time.fromMilliseconds 1;
+
+fun is_relevant {elapsed, cpu, gc} =
+  Time.>= (elapsed, min_time) orelse
+  Time.>= (cpu, min_time) orelse
+  Time.>= (gc, min_time);
+
 fun cond_timeit enabled msg e =
   if enabled then
     let
       val (timing, result) = timing (Exn.interruptible_capture e) ();
-      val end_msg = message timing;
-      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+      val _ =
+        if is_relevant timing then
+          let val end_msg = message timing
+          in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
+        else ();
     in Exn.release result end
   else e ();