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