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