# HG changeset patch
# User wenzelm
# Date 1520797637 -3600
# Node ID f9c071cc958b2fdb2986f0e36c7a59194d87b091
# Parent  661cd25304ae3697e7ba756fee1a54807149a434
update XML cache for slightly modified messages;

diff -r 661cd25304ae -r f9c071cc958b src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Mar 11 20:31:25 2018 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 11 20:47:17 2018 +0100
@@ -264,7 +264,8 @@
     def accumulate(
         self_id: Document_ID.Generic => Boolean,
         other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
-        message: XML.Elem): State =
+        message: XML.Elem,
+        xml_cache: XML.Cache): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -297,8 +298,8 @@
                       target_chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
-                          val info = Text.Info(range, XML.Elem(Markup(name, props), args))
-                          state.add_markup(false, target_name, info)
+                          val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+                          state.add_markup(false, target_name, Text.Info(range, elem))
                         case None => bad(); state
                       }
                     case _ =>
@@ -310,8 +311,8 @@
                 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
                   val range = command.proper_range
                   val props = Position.purge(atts)
-                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
-                  state.add_markup(false, Symbol.Text_Chunk.Default, info)
+                  val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+                  state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
 
                 case _ => bad(); state
               }
@@ -319,8 +320,10 @@
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
-              val markup_message = XML.Elem(Markup(Markup.message(name), props), body)
-              val message_markup = XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))
+              val markup_message =
+                xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
+              val message_markup =
+                xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
 
               var st = copy(results = results + (i -> markup_message))
               if (Protocol.is_inlined(message)) {
diff -r 661cd25304ae -r f9c071cc958b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Mar 11 20:31:25 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 11 20:47:17 2018 +0100
@@ -660,17 +660,18 @@
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
         graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
 
-    def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
+    def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
+      : (Command.State, State) =
     {
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st.accumulate(self_id(st), other_id _, message)
+          val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
           val execs1 = execs + (id -> new_st)
           (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st.accumulate(self_id(st), other_id _, message)
+              val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
               val commands1 = commands + (id -> new_st)
               (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
             case None => fail
diff -r 661cd25304ae -r f9c071cc958b src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Mar 11 20:31:25 2018 +0100
+++ b/src/Pure/PIDE/session.scala	Sun Mar 11 20:47:17 2018 +0100
@@ -412,7 +412,7 @@
       def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
       {
         try {
-          val st = global_state.change_result(_.accumulate(state_id, message))
+          val st = global_state.change_result(_.accumulate(state_id, message, xml_cache))
           change_buffer.invoke(false, List(st.command))
         }
         catch {