diff -r 389e660549d0 -r e69ebc4782a3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Sep 16 13:46:43 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 16 13:52:24 2025 +0200
@@ -1268,6 +1268,9 @@
       Document_Status.Command_Status.merge(
         command_states(version, command).iterator.map(_.document_status))
 
+    def command_timing(version: Version, command: Command): Timing =
+      Timing.merge(command_states(version, command).iterator.map(_.timing))
+
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))