--- a/src/Pure/PIDE/command.scala Wed Aug 25 22:37:53 2010 +0200
+++ b/src/Pure/PIDE/command.scala Wed Aug 25 22:45:24 2010 +0200
@@ -46,15 +46,12 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(Markup(name, atts), args) =>
- atts match {
- case Position.Range(range) if Position.Id.unapply(atts) == Some(command.id) =>
- val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
- val info =
- Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
- state.add_markup(info)
- case _ => System.err.println("Ignored report message: " + msg); state
- }
+ case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
+ if Position.Id.unapply(atts) == Some(command.id) =>
+ val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+ val info =
+ Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
+ state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
case _ => add_result(message)