suppress timing message in full PIDE protocol -- this is for batch build;
authorwenzelm
Tue, 19 Feb 2013 14:47:57 +0100
changeset 51219 2464ba6e6fc9
parent 51218 6425a0d3b7ac
child 51220 e140c8fa485a
suppress timing message in full PIDE protocol -- this is for batch build;
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 _ => ()