# HG changeset patch
# User wenzelm
# Date 1361281677 -3600
# Node ID 2464ba6e6fc92caadebdfb9ff5dd62b64fd004ea
# Parent  6425a0d3b7ac11e71d385308fd5966fb9d1ed1b8
suppress timing message in full PIDE protocol -- this is for batch build;

diff -r 6425a0d3b7ac -r 2464ba6e6fc9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 13:57:13 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 14:47:57 2013 +0100
@@ -624,7 +624,7 @@
 local
 
 fun timing_message tr t =
-  if Timing.is_relevant t then
+  if Timing.is_relevant t andalso not (Position.is_reported (pos_of tr)) then
     Output.protocol_message
       (Markup.command_timing :: approximative_id tr @ Markup.timing_properties t) ""
     handle Fail _ => ()