# HG changeset patch
# User wenzelm
# Date 1585759018 -7200
# Node ID 12c3fe42b2a8c2007e58dd321fb33eebd862614d
# Parent  7b0656fa783bd21b08a067024b650c9e816905ce
output prover messages;

diff -r 7b0656fa783b -r 12c3fe42b2a8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 18:22:19 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 18:36:58 2020 +0200
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import scala.collection.SortedSet
+import scala.collection.{SortedSet, mutable}
 import scala.annotation.tailrec
 
 
@@ -258,6 +258,22 @@
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
 
+          val stdout = new StringBuilder(1000)
+          val messages = new mutable.ListBuffer[String]
+
+          session.all_messages +=
+            Session.Consumer("build_session_output") {
+              case msg: Prover.Output =>
+                val message = msg.message
+                if (msg.is_stdout) {
+                  stdout ++= Symbol.encode(XML.content(message))
+                }
+                else if (Protocol.is_exported(message)) {
+                  messages += Symbol.encode(Protocol.message_text(List(message)))
+                }
+              case _ =>
+            }
+
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
@@ -268,7 +284,9 @@
 
           session.protocol_command("build_session", args_yxml)
 
-          val result = process.join
+          val process_result = process.join
+
+          val result = process_result.output(stdout.toString :: messages.toList)
           handler.build_session_errors.join match {
             case Nil => result
             case errors =>