# HG changeset patch
# User wenzelm
# Date 1758106851 -7200
# Node ID 887f1eac24d1d34593316346656fcd95b0c561bb
# Parent  47edc6384e7aa97facd40209ffe7e6ae1b4bd980
more scalable timing, as part of incremental document_status;

diff -r 47edc6384e7a -r 887f1eac24d1 src/Pure/PIDE/command.scala
--- 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)
 
diff -r 47edc6384e7a -r 887f1eac24d1 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Wed Sep 17 11:41:27 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 17 13:00:51 2025 +0200
@@ -53,6 +53,7 @@
       var canceled = false
       var forks = 0
       var runs = 0
+      var timing = Timing.zero
       for (markup <- markups) {
         markup.name match {
           case Markup.INITIALIZED =>
@@ -73,6 +74,10 @@
           case Markup.CANCELED => canceled = true
           case _ =>
         }
+        markup match {
+          case Markup.Timing(t) => timing += t
+          case _ =>
+        }
       }
       new Command_Status(
         theory_status = theory_status,
@@ -82,7 +87,8 @@
         failed = failed1,
         canceled = canceled,
         forks = forks,
-        runs = runs)
+        runs = runs,
+        timing = timing)
     }
 
     val empty: Command_Status = make()
@@ -99,7 +105,8 @@
     private val failed: Boolean,
     private val canceled: Boolean,
     val forks: Int,
-    val runs: Int
+    val runs: Int,
+    val timing: Timing
   ) extends Theory_Status {
     override def toString: String =
       if (is_empty) "Command_Status.empty"
@@ -110,7 +117,7 @@
     def is_empty: Boolean =
       !Theory_Status.initialized(theory_status) &&
       !touched && !accepted && !warned && !failed && !canceled &&
-      forks == 0 && runs == 0
+      forks == 0 && runs == 0 && timing.is_zero
 
     def + (that: Command_Status): Command_Status =
       if (is_empty) that
@@ -124,7 +131,8 @@
           failed = failed || that.failed,
           canceled = canceled || that.canceled,
           forks = forks + that.forks,
-          runs = runs + that.runs)
+          runs = runs + that.runs,
+          timing = timing + that.timing)
       }
 
     def update(
@@ -145,7 +153,8 @@
             failed = failed1,
             canceled = canceled,
             forks = forks,
-            runs = runs)
+            runs = runs,
+            timing = timing)
         }
       }
       else this + Command_Status.make(markups = markups, warned = warned, failed = failed)