--- a/src/Pure/PIDE/command.scala Wed Sep 22 22:25:21 2010 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 22 22:39:17 2010 +0200
@@ -60,10 +60,14 @@
atts match {
case Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+ val st0 = add_result(i, result)
val st1 =
- (add_result(i, result) /: Isar_Document.message_positions(command, message))(
- (st, range) => st.add_markup(Text.Info(range, result)))
- (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
+ if (Isar_Document.is_tracing(message)) st0
+ else
+ (st0 /: Isar_Document.message_positions(command, message))(
+ (st, range) => st.add_markup(Text.Info(range, result)))
+ val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
+ st2
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}