clarified signature;
more inlined protocol messages;

--- a/src/Pure/PIDE/session.scala	Wed Apr 01 21:10:44 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 01 21:43:22 2020 +0200
@@ -61,7 +61,10 @@
   /* events */
 
   //{{{
-  case class Statistics(props: Properties.T)
+  case class Command_Timing(props: Properties.T)
+  case class Theory_Timing(props: Properties.T)
+  case class Runtime_Statistics(props: Properties.T)
+  case class Task_Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
@@ -175,7 +178,10 @@
 
   /* outlets */
 
-  val statistics = new Session.Outlet[Session.Statistics](dispatcher)
+  val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
+  val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
+  val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
+  val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
@@ -480,11 +486,12 @@
                 init_protocol_handler(name)
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
+                command_timings.post(Session.Command_Timing(msg.properties))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
 
               case Protocol.Theory_Timing(_, _) =>
-                // FIXME
+                theory_timings.post(Session.Theory_Timing(msg.properties))
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
@@ -526,10 +533,10 @@
                 }
 
               case Markup.ML_Statistics(props) =>
-                statistics.post(Session.Statistics(props))
+                runtime_statistics.post(Session.Runtime_Statistics(props))
 
               case Markup.Task_Statistics(props) =>
-                // FIXME
+                task_statistics.post(Session.Task_Statistics(props))
 
               case _ => bad_output()
             }

--- a/src/Pure/Tools/build.scala	Wed Apr 01 21:10:44 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 21:43:22 2020 +0200
@@ -259,9 +259,13 @@
 
           val stdout = new StringBuilder(1000)
           val messages = new mutable.ListBuffer[String]
+          val command_timings = new mutable.ListBuffer[Properties.T]
+          val theory_timings = new mutable.ListBuffer[Properties.T]
+          val runtime_statistics = new mutable.ListBuffer[Properties.T]
+          val task_statistics = new mutable.ListBuffer[Properties.T]
 
-          session.all_messages +=
-            Session.Consumer("build_session_output") {
+          val consumer =
+            Session.Consumer[Any]("build_session_output") {
               case msg: Prover.Output =>
                 val message = msg.message
                 if (msg.is_stdout) {
@@ -271,9 +275,19 @@
                   messages +=
                     Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))
                 }
+              case Session.Command_Timing(props) => command_timings += props
+              case Session.Theory_Timing(props) => theory_timings += props
+              case Session.Runtime_Statistics(props) => runtime_statistics += props
+              case Session.Task_Statistics(props) => task_statistics += props
               case _ =>
             }
 
+          session.all_messages += consumer
+          session.command_timings += consumer
+          session.theory_timings += consumer
+          session.runtime_statistics += consumer
+          session.task_statistics += consumer
+
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
@@ -285,8 +299,14 @@
           session.protocol_command("build_session", args_yxml)
 
           val process_result = process.join
+          val process_output =
+            stdout.toString :: messages.toList :::
+            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) :::
+            task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
-          val result = process_result.output(stdout.toString :: messages.toList)
+          val result = process_result.output(process_output)
           handler.build_session_errors.join match {
             case Nil => result
             case errors =>

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 01 21:10:44 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 01 21:43:22 2020 +0200
@@ -108,7 +108,7 @@
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
-      case stats: Session.Statistics =>
+      case stats: Session.Runtime_Statistics =>
         add_statistics(stats.props)
         update_delay.invoke()
 
@@ -118,13 +118,13 @@
 
   override def init()
   {
-    PIDE.session.statistics += main
+    PIDE.session.runtime_statistics += main
     PIDE.session.global_options += main
   }
 
   override def exit()
   {
-    PIDE.session.statistics -= main
+    PIDE.session.runtime_statistics -= main
     PIDE.session.global_options -= main
   }
 }