diff -r 7a2bd0d12f18 -r 7f46426e69ab src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Sep 20 18:15:23 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Sep 20 18:38:45 2025 +0200
@@ -78,13 +78,9 @@
   /* command timing */
 
   object Command_Timing {
-    def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] =
+    def unapply(props: Properties.T): Option[(Document_ID.Generic, Properties.T)] =
       props match {
-        case Markup.Command_Timing(args) =>
-          (args, args) match {
-            case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing))
-            case _ => None
-          }
+        case Markup.Command_Timing(args@Position.Id(id)) => Some((id, args))
         case _ => None
       }
   }