# HG changeset patch
# User wenzelm
# Date 1596831572 -7200
# Node ID 7773ec172572e7c0f22d8a248aea3e114d5cab8a
# Parent  c998827f1df9a285c32af6a87cf4839149157183
clarified names;
removed remains of old protocol messages;

diff -r c998827f1df9 -r 7773ec172572 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:19:32 2020 +0200
@@ -75,17 +75,17 @@
       }
     }
 
-    private def ml_pid(msg: Prover.Protocol_Output): Boolean = synchronized
+    private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.ML_Pid(pid) =>
+        case Markup.ML_Statistics(pid) =>
           monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) }
           true
         case _ => false
       }
     }
 
-    val functions = List(Markup.ML_Pid.name -> ml_pid)
+    val functions = List(Markup.ML_Statistics.name -> ml_statistics)
   }
 
 
diff -r c998827f1df9 -r 7773ec172572 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 07 22:19:32 2020 +0200
@@ -209,14 +209,13 @@
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
-  val ml_pid: int -> Properties.T
+  val ML_statistics: {pid: int} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val protocol_handler: string -> Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
-  val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
@@ -673,7 +672,7 @@
 
 val functionN = "function"
 
-fun ml_pid pid = [(functionN, "ML_pid"), (idN, Value.print_int pid)];
+fun ML_statistics {pid} = [(functionN, "ML_statistics"), ("pid", Value.print_int pid)];
 
 val commands_accepted = [(functionN, "commands_accepted")];
 
@@ -685,8 +684,6 @@
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
-val ML_statistics = (functionN, "ML_statistics");
-
 val task_statistics = (functionN, "task_statistics");
 
 val command_timing = (functionN, "command_timing");
diff -r c998827f1df9 -r 7773ec172572 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 07 22:19:32 2020 +0200
@@ -576,11 +576,11 @@
       }
   }
 
-  object ML_Pid extends Function("ML_pid")
+  object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
-        case List(PROPERTY, (ID, Value.Long(pid))) => Some(pid)
+        case List(PROPERTY, ("pid", Value.Long(pid))) => Some(pid)
         case _ => None
       }
   }
@@ -593,7 +593,6 @@
   {
     val Threads = new Properties.Int("threads")
   }
-  object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Name_Function("loading_theory")
diff -r c998827f1df9 -r 7773ec172572 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Aug 07 22:19:32 2020 +0200
@@ -495,9 +495,6 @@
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
 
-              case Markup.ML_Statistics(props) =>
-                runtime_statistics.post(Session.Runtime_Statistics(props))
-
               case Markup.Task_Statistics(props) =>
                 task_statistics.post(Session.Task_Statistics(props))
 
diff -r c998827f1df9 -r 7773ec172572 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 07 22:19:32 2020 +0200
@@ -201,7 +201,7 @@
 
     fun protocol () =
      (Session.init_protocol_handlers ();
-      Output.protocol_message (Markup.ml_pid (ML_Pid.get ())) [];
+      Output.protocol_message (Markup.ML_statistics {pid = ML_Pid.get ()}) [];
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());
 
diff -r c998827f1df9 -r 7773ec172572 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Aug 07 22:19:32 2020 +0200
@@ -316,10 +316,14 @@
                 fun(Markup.Command_Timing.name, command_timings, command_timing),
                 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))
           })
 
+        session.runtime_statistics += Session.Consumer("ML_statistics")
+          {
+            case Session.Runtime_Statistics(props) => runtime_statistics += props
+          }
+
         session.all_messages += Session.Consumer[Any]("build_session_output")
           {
             case msg: Prover.Output =>