# HG changeset patch
# User wenzelm
# Date 1594212182 -7200
# Node ID 5c4800f6b25a9edfa3c2c5a634a26f522d208022
# Parent  3e08311ada8ec8209d01e3ba45901b1073002dc0
more robust protocol for "Timing ..." messages, notably for pide_session=true;

diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Jul 08 14:43:02 2020 +0200
@@ -223,6 +223,7 @@
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
+  val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
@@ -705,6 +706,8 @@
 
 val theory_timing = (functionN, "theory_timing");
 
+val session_timing = (functionN, "session_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 08 14:43:02 2020 +0200
@@ -575,6 +575,7 @@
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
+  object Session_Timing extends Properties_Function("session_timing")
   object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")
 
diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/System/process_result.scala	Wed Jul 08 14:43:02 2020 +0200
@@ -42,7 +42,8 @@
     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
   def errors(errs: List[String]): Process_Result =
     copy(err_lines = err_lines ::: errs.flatMap(split_lines))
-  def error(err: String): Process_Result = errors(List(err))
+  def error(err: String): Process_Result =
+    if (err.isEmpty) this else errors(List(err))
 
   def was_timeout: Process_Result = copy(rc = 1, timeout = true)
 
diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/Tools/build.ML	Wed Jul 08 14:43:02 2020 +0200
@@ -58,7 +58,7 @@
 
     val timing_props =
       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
-    val _ = Protocol_Message.marker "Timing" timing_props;
+    val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
@@ -93,6 +93,8 @@
         end
       else if function = Markup.theory_timing then
         Protocol_Message.marker (#2 function) args
+      else if function = Markup.session_timing then
+        Protocol_Message.marker "Timing" args
       else
         (case Markup.dest_loading_theory props of
           SOME name => Protocol_Message.marker_text "loading_theory" name
diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 08 14:43:02 2020 +0200
@@ -226,9 +226,11 @@
 
           val build_session_errors: Promise[List[String]] = Future.promise
           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]
+          val session_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
           val task_statistics = new mutable.ListBuffer[Properties.T]
 
@@ -294,6 +296,7 @@
                   Markup.EXPORT -> export,
                   fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply),
                   fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
+                  fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
                   fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),
                   fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
             })
@@ -305,6 +308,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
                 }
@@ -337,10 +343,12 @@
               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) :::
+            session_timings.toList.map(Protocol.Timing_Marker.apply) :::
             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