tuned;

--- a/src/Pure/PIDE/command.scala	Sun Mar 11 20:47:17 2018 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 11 20:56:42 2018 +0100
@@ -251,6 +251,9 @@
     private def add_status(st: Markup): State =
       copy(status = st :: status)
 
+    private def add_result(entry: Results.Entry): State =
+      copy(results = results + entry)
+
     private def add_markup(
       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
     {
@@ -325,7 +328,7 @@
               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))
+              var st = add_result(i -> markup_message)
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator