--- a/src/Pure/PIDE/command.scala Tue Sep 07 16:08:29 2010 +0200
+++ b/src/Pure/PIDE/command.scala Tue Sep 07 16:40:30 2010 +0200
@@ -60,8 +60,8 @@
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.id, message))(
- (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+ (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
+ (st, range) => st.add_markup(Text.Info(range, result)))
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}