src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Wed Aug 24 13:40:10 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 15:30:43 2011 +0200
@@ -275,7 +275,8 @@
 
 local
 
-fun timing tr t = Toplevel.status tr (Markup.timing t);
+fun timing tr t =
+  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
 
 fun proof_status tr st =
   (case try Toplevel.proof_of st of