suppress timing message in full PIDE protocol -- this is for batch build;
authorwenzelm
Tue Feb 19 14:47:57 2013 +0100 (2013-02-19 ago)
changeset 512192464ba6e6fc9
parent 51218 6425a0d3b7ac
child 51220 e140c8fa485a
suppress timing message in full PIDE protocol -- this is for batch build;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 13:57:13 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 14:47:57 2013 +0100
     1.3 @@ -624,7 +624,7 @@
     1.4  local
     1.5  
     1.6  fun timing_message tr t =
     1.7 -  if Timing.is_relevant t then
     1.8 +  if Timing.is_relevant t andalso not (Position.is_reported (pos_of tr)) then
     1.9      Output.protocol_message
    1.10        (Markup.command_timing :: approximative_id tr @ Markup.timing_properties t) ""
    1.11      handle Fail _ => ()