--- a/src/Pure/PIDE/command.scala Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Pure/PIDE/command.scala Fri Sep 17 17:10:44 2010 +0200
@@ -60,8 +60,10 @@
atts match {
case Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
- (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
- (st, range) => st.add_markup(Text.Info(range, 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 _)
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}