# HG changeset patch
# User wenzelm
# Date 1418933439 -3600
# Node ID 0070053570c41383378652ec0d56625b31b63a26
# Parent  7a373a35a37a12f9ba653d29b161b71f8692c03b
suppress irrelevant timing messages (the majority);

diff -r 7a373a35a37a -r 0070053570c4 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Thu Dec 18 17:26:53 2014 +0100
+++ b/src/Pure/General/timing.ML	Thu Dec 18 21:10:39 2014 +0100
@@ -105,7 +105,9 @@
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
 fun protocol_message props t =
-  Output.try_protocol_message (props @ Markup.timing_properties t) [];
+  if is_relevant t then
+    Output.try_protocol_message (props @ Markup.timing_properties t) []
+  else ();
 
 fun protocol props f x =
   let
diff -r 7a373a35a37a -r 0070053570c4 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Dec 18 17:26:53 2014 +0100
+++ b/src/Pure/Tools/build.ML	Thu Dec 18 21:10:39 2014 +0100
@@ -82,9 +82,11 @@
           val pos = Position.of_properties args;
           val {elapsed, ...} = Markup.parse_timing_properties args;
         in
-          (case approximative_id name pos of
-            SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
-          | NONE => ())
+          if Timing.is_relevant_time elapsed then
+            (case approximative_id name pos of
+              SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
+            | NONE => ())
+          else ()
         end
       else
         (case Markup.dest_loading_theory props of