retain original messages properties, e.g. for retrieval via Command.Results;
authorwenzelm
Fri, 09 Aug 2013 10:41:17 +0200
changeset 52930 5fab62ae3532
parent 52929 52d21bddcb8a
child 52931 ac6648c0c0fb
retain original messages properties, e.g. for retrieval via Command.Results;
src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 09 09:55:25 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 09 10:41:17 2013 +0200
@@ -111,10 +111,9 @@
                 // FIXME java.lang.System.err.println("Ignored report message: " + msg)
                 state
             })
-        case XML.Elem(Markup(name, atts), body) =>
-          atts match {
+        case XML.Elem(Markup(name, props), body) =>
+          props match {
             case Markup.Serial(i) =>
-              val props = Position.purge(atts)
               val message1 = XML.Elem(Markup(Markup.message(name), props), body)
               val message2 = XML.Elem(Markup(name, props), body)