src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 31 23:28:21 2010 +0200
@@ -48,8 +48,8 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
-              if Position.Id.unapply(atts) == Some(command.id) =>
+              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
+              if id == command.id =>
                 val props = Position.purge(atts)
                 val info =
                   Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
@@ -59,7 +59,9 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Markup.Serial(i) =>
-              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
+              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)))
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }