more scalable Command.State.document_status: prefer incremental update;
clarified signature;

--- a/src/Pure/PIDE/command.scala	Tue Sep 16 20:33:36 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 16 21:04:39 2025 +0200
@@ -49,6 +49,9 @@
       args.iterator.foldLeft(empty)(_ + _)
     def merge(args: IterableOnce[Results]): Results =
       args.iterator.foldLeft(empty)(_ ++ _)
+
+    def warned(entry: Entry): Boolean = Protocol.is_warning_or_legacy(entry._2)
+    def failed(entry: Entry): Boolean = Protocol.is_error(entry._2)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem]) {
@@ -57,8 +60,8 @@
     def get(serial: Long): Option[XML.Elem] = rep.get(serial)
     def iterator: Iterator[Results.Entry] = rep.iterator
 
-    lazy val warned: Boolean = rep.exists(p => Protocol.is_warning_or_legacy(p._2))
-    lazy val failed: Boolean = rep.exists(p => Protocol.is_error(p._2))
+    def warned: Boolean = rep.exists(Results.warned)
+    def failed: Boolean = rep.exists(Results.failed)
 
     def + (entry: Results.Entry): Results =
       if (defined(entry._1)) this
@@ -214,7 +217,14 @@
       results: Results = Results.empty,
       exports: Exports = Exports.empty,
       markups: Markups = Markups.empty
-    ): State = new State(command, status, results, exports, markups)
+    ): State = {
+      val document_status =
+        Document_Status.Command_Status.make(
+          markups = status,
+          warned = results.warned,
+          failed = results.failed)
+      new State(command, status, results, exports, markups, document_status)
+    }
   }
 
   final class State private(
@@ -222,7 +232,8 @@
     val status: List[Markup],
     val results: Results,
     val exports: Exports,
-    val markups: Markups
+    val markups: Markups,
+    val document_status: Document_Status.Command_Status
   ) {
     override def toString: String = "Command.State(" + command + ")"
     override def hashCode(): Int = ???
@@ -234,10 +245,6 @@
         case (t0, _) => t0
       }
 
-    lazy val document_status: Document_Status.Command_Status =
-      Document_Status.Command_Status.make(
-        status, warned = results.warned, failed = results.failed)
-
     def initialized: Boolean = document_status.initialized
     def consolidating: Boolean = document_status.consolidating
     def consolidated: Boolean = document_status.consolidated
@@ -251,15 +258,28 @@
       else Some(State(other_command, markups = markups1))
     }
 
-    private def add_status(st: Markup): State =
-      new State(command, st :: status, results, exports, markups)
+    private def add_status(st: Markup): State = {
+      val document_status1 =
+        document_status + Document_Status.Command_Status.make(markups = List(st))
+      new State(command, st :: status, results, exports, markups, document_status1)
+    }
 
-    private def add_result(entry: Results.Entry): State =
-      new State(command, status, results + entry, exports, markups)
+    private def add_result(entry: Results.Entry): State = {
+      val warned = document_status.is_warned || Results.warned(entry)
+      val failed = document_status.is_failed || Results.failed(entry)
+      val document_status1 =
+        if (warned == document_status.is_warned && failed == document_status.is_failed) {
+          document_status
+        }
+        else {
+          document_status + Document_Status.Command_Status.make(warned = warned, failed = failed)
+        }
+      new State(command, status, results + entry, exports, markups, document_status1)
+    }
 
     def add_export(entry: Exports.Entry): Option[State] =
       if (command.node_name.theory == entry._2.theory_name) {
-        Some(new State(command, status, results, exports + entry, markups))
+        Some(new State(command, status, results, exports + entry, markups, document_status))
       }
       else None
 
@@ -273,7 +293,7 @@
           markups.add(Markup_Index(true, chunk_name), m)
         else markups
       val markups2 = markups1.add(Markup_Index(false, chunk_name), m)
-      new State(command, this.status, results, exports, markups2)
+      new State(command, this.status, results, exports, markups2, document_status)
     }
 
     def accumulate(

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 20:33:36 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 21:04:39 2025 +0200
@@ -41,7 +41,7 @@
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
     def make(
-      markups: Iterable[Markup],
+      markups: Iterable[Markup] = Nil,
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
@@ -85,7 +85,7 @@
         runs = runs)
     }
 
-    val empty: Command_Status = make(Nil)
+    val empty: Command_Status = make()
 
     def merge(args: IterableOnce[Command_Status]): Command_Status =
       args.iterator.foldLeft(empty)(_ + _)

--- a/src/Pure/PIDE/rendering.scala	Tue Sep 16 20:33:36 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Sep 16 21:04:39 2025 +0200
@@ -510,7 +510,7 @@
       color <-
         result match {
           case (markups, opt_color) if markups.nonEmpty =>
-            val status = Document_Status.Command_Status.make(markups)
+            val status = Document_Status.Command_Status.make(markups = markups)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
             else if (status.is_running) Some(Rendering.Color.running1)
             else if (status.is_canceled) Some(Rendering.Color.canceled)
@@ -772,7 +772,7 @@
             }, status = true)
       if (results.isEmpty) None
       else {
-        val status = Document_Status.Command_Status.make(results.flatMap(_.info))
+        val status = Document_Status.Command_Status.make(markups = results.flatMap(_.info))
 
         if (status.is_running) Some(Rendering.Color.running)
         else if (status.is_failed) Some(Rendering.Color.error)