# HG changeset patch # User wenzelm # Date 1353526612 -3600 # Node ID 7b61a539721efb184a32c07b167bec064ab3cc2b # Parent 76efdb6daab2288111eb0063ea5138d3d1e79f45 always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window; diff -r 76efdb6daab2 -r 7b61a539721e src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Nov 21 20:15:25 2012 +0100 +++ b/src/Pure/PIDE/command.scala Wed Nov 21 20:36:52 2012 +0100 @@ -66,15 +66,14 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), atts), body) - val message2 = XML.Elem(Markup(name, Position.purge(atts)), body) - - val st0 = copy(results = results + (i -> message1)) + val st0 = + copy(results = + results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body))) val st1 = if (Protocol.is_tracing(message)) st0 else (st0 /: Protocol.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, message2))) + (st, range) => st.add_markup(Text.Info(range, message))) st1 case _ => System.err.println("Ignored message without serial number: " + message); this