--- a/src/Pure/PIDE/command.scala Tue Sep 16 12:32:13 2025 +0200
+++ b/src/Pure/PIDE/command.scala Tue Sep 16 13:46:43 2025 +0200
@@ -213,6 +213,12 @@
exports: Exports = Exports.empty,
markups: Markups = Markups.empty
) {
+ lazy val timing: Timing =
+ status.foldLeft(Timing.zero) {
+ case (t0, Markup.Timing(t)) => t0 + t
+ case (t0, _) => t0
+ }
+
lazy val document_status: Document_Status.Command_Status =
Document_Status.Command_Status.make(
status, warned = results.warned, failed = results.failed)