--- a/src/Pure/PIDE/command.scala Wed Sep 17 11:41:27 2025 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 17 13:00:51 2025 +0200
@@ -239,16 +239,11 @@
override def hashCode(): Int = ???
override def equals(obj: Any): Boolean = ???
- lazy val timing: Timing =
- status.foldLeft(Timing.zero) {
- case (t0, Markup.Timing(t)) => t0 + t
- case (t0, _) => t0
- }
-
def initialized: Boolean = document_status.initialized
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 markup(index: Markup_Index): Markup_Tree = markups(index)