--- 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)
}
--- 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");
--- 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")
--- 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))
--- 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 ());
--- 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 =>