src/Pure/PIDE/command.scala
changeset 38722 ba31936497c2
parent 38714 31da698fc4e5
child 38723 6a55b8978a56
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 25 21:31:22 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 25 22:37:53 2010 +0200
     1.3 @@ -46,12 +46,15 @@
     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), args)
     1.8 -              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
     1.9 -                val range = command.decode(Position.get_range(atts).get)
    1.10 -                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    1.11 -                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    1.12 -                state.add_markup(info)
    1.13 +              case XML.Elem(Markup(name, atts), args) =>
    1.14 +                atts match {
    1.15 +                  case Position.Range(range) if Position.Id.unapply(atts) == Some(command.id) =>
    1.16 +                    val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    1.17 +                    val info =
    1.18 +                      Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    1.19 +                    state.add_markup(info)
    1.20 +                  case _ => System.err.println("Ignored report message: " + msg); state
    1.21 +                }
    1.22                case _ => System.err.println("Ignored report message: " + msg); state
    1.23              })
    1.24          case _ => add_result(message)