src/Pure/Isar/toplevel.ML
changeset 51219 2464ba6e6fc9
parent 51217 65ab2c4f4c32
child 51222 8c3e5fb41139
     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 _ => ()