# HG changeset patch
# User wenzelm
# Date 1593025190 -7200
# Node ID 3e54088a7119a6f5859c4e2751ac257937a9532f
# Parent  c5003c5c72c8738040de5f34a92a61f052337f2e
clarified use of memory: prefer share tree structures over fresh strings;

diff -r c5003c5c72c8 -r 3e54088a7119 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jun 24 11:16:57 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jun 24 20:59:50 2020 +0200
@@ -226,7 +226,7 @@
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)
-          val messages = new mutable.ListBuffer[String]
+          val messages = new mutable.ListBuffer[XML.Elem]
           val command_timings = new mutable.ListBuffer[Properties.T]
           val theory_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
@@ -306,8 +306,7 @@
                   stdout ++= Symbol.encode(XML.content(message))
                 }
                 else if (Protocol.is_exported(message)) {
-                  messages +=
-                    Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))
+                  messages += message
                 }
               case _ =>
             }
@@ -333,7 +332,9 @@
           val process_result =
             Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
           val process_output =
-            stdout.toString :: messages.toList :::
+            stdout.toString ::
+            messages.toList.map(message =>
+              Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::