more accurate theory timing, based on sum of command timings;
remove obsolete protocol message;

--- a/src/Pure/Build/build_job.scala	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Wed Sep 24 16:22:49 2025 +0200
@@ -214,7 +214,6 @@
           val stdout = new StringBuilder(1000)
           val stderr = new StringBuilder(1000)
           val command_timings = new mutable.ListBuffer[Properties.T]
-          val theory_timings = new mutable.ListBuffer[Properties.T]
           val session_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
           val task_statistics = new mutable.ListBuffer[Properties.T]
@@ -222,7 +221,7 @@
           var nodes_status = Document_Status.Nodes_Status.empty
 
           val nodes_domain =
-            build_context.deps(session_name).used_theories.map(_._1.symbolic_path)
+            session_background.base.used_theories.map(_._1.symbolic_path)
 
           def nodes_status_progress(): Unit = {
             val state = session.get_state()
@@ -309,7 +308,6 @@
                   Markup.Build_Session_Finished.name -> build_session_finished,
                   Markup.Loading_Theory.name -> loading_theory,
                   Markup.EXPORT -> export_,
-                  fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
                   fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
                   fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
             })
@@ -470,18 +468,13 @@
           /* process result */
 
           val result1 = {
-            val theory_timing =
-              theory_timings.iterator.flatMap(
-                {
-                  case props @ Markup.Name(name) => Some(name -> props)
-                  case _ => None
-                }).toMap
-            val used_theory_timings =
-              for { (name, _) <- session_background.base.used_theories }
-                yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
-
             val more_output =
               session.synchronized {
+                val used_theory_timings =
+                  nodes_domain.map(name =>
+                    Markup.Name(name.theory) :::
+                    Markup.Timing_Properties(nodes_status(name).total_timing))
+
                 Library.trim_line(stdout.toString) ::
                   command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
                   used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 24 16:22:49 2025 +0200
@@ -237,7 +237,7 @@
       var finished = 0
       var canceled = false
       var terminated = true
-      var total_time = Time.zero
+      var total_timing = Timing.zero
       var max_time = Time.zero
       var command_timings = Map.empty[Command, Command_Timings]
 
@@ -256,7 +256,7 @@
         if (!status.is_terminated) terminated = false
 
         val t = status.timings.sum.elapsed
-        total_time += t
+        total_timing += status.timings.sum
         if (t > max_time) max_time = t
         if (t.is_notable(threshold)) command_timings += (command -> status.timings)
       }
@@ -271,7 +271,7 @@
         finished = finished,
         canceled = canceled,
         terminated = terminated,
-        total_time = total_time,
+        total_timing = total_timing,
         max_time = max_time,
         threshold = threshold,
         command_timings = command_timings)
@@ -288,7 +288,7 @@
     finished: Int = 0,
     canceled: Boolean = false,
     terminated: Boolean = false,
-    total_time: Time = Time.zero,
+    total_timing: Timing = Timing.zero,
     max_time: Time = Time.zero,
     threshold: Time = Time.zero,
     command_timings: Map[Command, Command_Timings] = Map.empty

--- a/src/Pure/PIDE/markup.ML	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Sep 24 16:22:49 2025 +0200
@@ -264,7 +264,6 @@
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
-  val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
@@ -833,8 +832,6 @@
 
 val command_timing = function "command_timing";
 
-val theory_timing = function "theory_timing";
-
 val session_timing = function "session_timing";
 
 fun loading_theory name = [function "loading_theory", (nameN, name)];

--- a/src/Pure/PIDE/markup.scala	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Sep 24 16:22:49 2025 +0200
@@ -716,7 +716,6 @@
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
-  object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing") {
     val Threads = new Properties.Int("threads")
   }

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

--- a/src/Pure/System/progress.scala	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/System/progress.scala	Wed Sep 24 16:22:49 2025 +0200
@@ -65,7 +65,7 @@
 
     def theory(name: Document.Node.Name): Theory = {
       val node_status = apply(name)
-      Theory(theory = name.theory, session = session, total_time = node_status.total_time)
+      Theory(theory = name.theory, session = session, total_time = node_status.total_timing.elapsed)
     }
   }
 }

--- a/src/Pure/Thy/thy_info.ML	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 24 16:22:49 2025 +0200
@@ -372,17 +372,11 @@
         (parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
           Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();
 
-    val timing_start = Timing.start ();
-
     val header = Thy_Header.make (name, put_id header_pos) imports keywords;
     val (theory, present) =
       eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
-    val timing_result = Timing.result timing_start;
-    val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
-    val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
-
     fun commit segments =
       update_thy deps (theory,
         if Options.bool options \<^system_option>\<open>record_theories\<close> then segments else []);

--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 23 13:11:52 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 24 16:22:49 2025 +0200
@@ -145,7 +145,7 @@
     val theories =
       List.from(
         for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
-          yield Theory_Entry(a, st.total_time.seconds)).sorted(Entry.Ordering)
+          yield Theory_Entry(a, st.total_timing.elapsed.seconds)).sorted(Entry.Ordering)
     val commands =
       (for ((command, timings) <- nodes_status(name).command_timings.toList)
         yield Command_Entry(command, timings.sum.elapsed.seconds)).sorted(Entry.Ordering)