tuned;
authorwenzelm
Sun Mar 11 20:56:42 2018 +0100 (17 months ago ago)
changeset 678265ea76b219668
parent 67825 f9c071cc958b
child 67827 b027c97c77c9
tuned;
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 11 20:47:17 2018 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 11 20:56:42 2018 +0100
     1.3 @@ -251,6 +251,9 @@
     1.4      private def add_status(st: Markup): State =
     1.5        copy(status = st :: status)
     1.6  
     1.7 +    private def add_result(entry: Results.Entry): State =
     1.8 +      copy(results = results + entry)
     1.9 +
    1.10      private def add_markup(
    1.11        status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
    1.12      {
    1.13 @@ -325,7 +328,7 @@
    1.14                val message_markup =
    1.15                  xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
    1.16  
    1.17 -              var st = copy(results = results + (i -> markup_message))
    1.18 +              var st = add_result(i -> markup_message)
    1.19                if (Protocol.is_inlined(message)) {
    1.20                  for {
    1.21                    (chunk_name, chunk) <- command.chunks.iterator