# HG changeset patch
# User wenzelm
# Date 1376037677 -7200
# Node ID 5fab62ae3532e725abab7fc5297ac2306f47691f
# Parent  52d21bddcb8ac693d08c0d4dbff4847334d73c19
retain original messages properties, e.g. for retrieval via Command.Results;

diff -r 52d21bddcb8a -r 5fab62ae3532 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)