diff -r cde288fef097 -r a39fde2f020a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Sep 21 19:47:26 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Sep 21 23:48:59 2025 +0200
@@ -63,7 +63,7 @@
   /* events */
 
   //{{{
-  case class Command_Timing(props: Properties.T)
+  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)
@@ -538,7 +538,7 @@
               case Protocol.Command_Timing(state_id, props) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.elem(Markup(Markup.TIMING, props))))
                 change_command(_.accumulate(state_id, cache.elem(message), cache))
-                command_timings.post(Session.Command_Timing(props))
+                command_timings.post(Session.Command_Timing(state_id, props))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))