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