recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);
authorwenzelm
Thu, 06 Aug 2020 23:44:43 +0200
changeset 72108 411b3dc036ca
parent 72107 1b06ed254943
child 72109 ae683a461c40
recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Aug 06 23:27:52 2020 +0200
+++ b/src/Pure/Tools/build.scala	Thu Aug 06 23:44:43 2020 +0200
@@ -237,6 +237,7 @@
         }
 
         val stdout = new StringBuilder(1000)
+        val stderr = new StringBuilder(1000)
         val messages = new mutable.ListBuffer[XML.Elem]
         val command_timings = new mutable.ListBuffer[Properties.T]
         val theory_timings = new mutable.ListBuffer[Properties.T]
@@ -326,6 +327,9 @@
               if (msg.is_stdout) {
                 stdout ++= Symbol.encode(XML.content(message))
               }
+              else if (msg.is_stderr) {
+                stderr ++= Symbol.encode(XML.content(message))
+              }
               else if (Protocol.is_exported(message)) {
                 messages += message
               }
@@ -371,7 +375,8 @@
           runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
           task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
-        val result = process_result.output(process_output)
+        val result =
+          process_result.output(process_output).error(Library.trim_line(stderr.toString))
 
         errors match {
           case Exn.Res(Nil) => result