src/Pure/PIDE/command.scala
changeset 38887 1261481ef5e5
parent 38877 682c4932b3cc
child 39172 31b95e0da7b7
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 31 22:03:55 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 31 23:28:21 2010 +0200
     1.3 @@ -48,8 +48,8 @@
     1.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     1.5            (this /: msgs)((state, msg) =>
     1.6              msg match {
     1.7 -              case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
     1.8 -              if Position.Id.unapply(atts) == Some(command.id) =>
     1.9 +              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
    1.10 +              if id == command.id =>
    1.11                  val props = Position.purge(atts)
    1.12                  val info =
    1.13                    Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    1.14 @@ -59,7 +59,9 @@
    1.15          case XML.Elem(Markup(name, atts), body) =>
    1.16            atts match {
    1.17              case Markup.Serial(i) =>
    1.18 -              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
    1.19 +              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    1.20 +              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
    1.21 +                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
    1.22              case _ => System.err.println("Ignored message without serial number: " + message); this
    1.23            }
    1.24        }