--- a/src/Pure/PIDE/command.scala Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/PIDE/command.scala Thu Nov 22 13:21:02 2012 +0100
@@ -66,14 +66,16 @@
case XML.Elem(Markup(name, atts), body) =>
atts match {
case Isabelle_Markup.Serial(i) =>
- val st0 =
- copy(results =
- results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body)))
+ val props = Position.purge(atts)
+ val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+ val message2 = XML.Elem(Markup(name, props), body)
+
+ val st0 = copy(results = results + (i -> message1))
val st1 =
if (Protocol.is_tracing(message)) st0
else
(st0 /: Protocol.message_positions(command, message))(
- (st, range) => st.add_markup(Text.Info(range, message)))
+ (st, range) => st.add_markup(Text.Info(range, message2)))
st1
case _ => System.err.println("Ignored message without serial number: " + message); this