src/Pure/PIDE/command.scala
changeset 39172 31b95e0da7b7
parent 38887 1261481ef5e5
child 39173 ed3946086358
--- 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
           }
       }