diff -r a39fde2f020a -r 9cc5d77d505c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Sep 21 23:48:59 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 22 14:01:37 2025 +0200
@@ -243,7 +243,7 @@
     def consolidating: Boolean = document_status.consolidating
     def consolidated: Boolean = document_status.consolidated
     def maybe_consolidated: Boolean = document_status.maybe_consolidated
-    def timing: Timing = document_status.timing
+    def timings: Document_Status.Command_Timings = document_status.timings
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)