retain original messages properties, e.g. for retrieval via Command.Results;
--- 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)