# HG changeset patch
# User wenzelm
# Date 1361881644 -3600
# Node ID 3d3c1ea0a4013041e7dc014096084168c0c99b74
# Parent  c05f7e1dd6023d8396832d5c1893071049a88318
tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;

diff -r c05f7e1dd602 -r 3d3c1ea0a401 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Feb 26 13:05:48 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 26 13:27:24 2013 +0100
@@ -637,8 +637,7 @@
 local
 
 fun timing_message tr (t: Timing.timing) =
-  if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
-  then
+  if Timing.is_relevant_time (#elapsed t) then
     (case approximative_id tr of
       SOME id =>
         (Output.protocol_message