# 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