# HG changeset patch
# User wenzelm
# Date 1282769124 -7200
# Node ID 6a55b8978a5669ba53a5a139f5a6240b1e7362c9
# Parent  ba31936497c2b32313ddddcd3c8d030a298e0af3
tuned;

diff -r ba31936497c2 -r 6a55b8978a56 src/Pure/PIDE/command.scala
--- 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)