--- a/src/Pure/PIDE/session.scala Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/PIDE/session.scala Wed Sep 24 16:22:49 2025 +0200
@@ -64,7 +64,6 @@
//{{{
case class Command_Timing(state_id: Document_ID.Generic, 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)
@@ -239,7 +238,6 @@
val finished_theories = new Session.Outlet[Document.Snapshot](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)
@@ -540,9 +538,6 @@
change_command(_.accumulate(state_id, cache.elem(message), cache))
command_timings.post(Session.Command_Timing(state_id, props))
- case Markup.Theory_Timing(props) =>
- theory_timings.post(Session.Theory_Timing(props))
-
case Markup.Task_Statistics(props) =>
task_statistics.post(Session.Task_Statistics(props))