--- 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()
}