minor performance tuning;

--- a/src/Pure/PIDE/command.scala	Mon Sep 15 17:42:09 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 15 18:09:55 2025 +0200
@@ -57,6 +57,9 @@
     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(p._2) || Protocol.is_legacy(p._2))
+    lazy val failed: Boolean = rep.exists(p => Protocol.is_error(p._2))
+
     def + (entry: Results.Entry): Results =
       if (defined(entry._1)) this
       else new Results(rep + entry)
@@ -230,17 +233,9 @@
       touched && forks == 0 && runs == 0
     }
 
-    lazy val document_status: Document_Status.Command_Status = {
-      val warnings =
-        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
-          List(Markup(Markup.WARNING, Nil))
-        else Nil
-      val errors =
-        if (results.iterator.exists(p => Protocol.is_error(p._2)))
-          List(Markup(Markup.ERROR, Nil))
-        else Nil
-      Document_Status.Command_Status.make(warnings ::: errors ::: status)
-    }
+    lazy val document_status: Document_Status.Command_Status =
+      Document_Status.Command_Status.make(
+        status, warned = results.warned, failed = results.failed)
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 

--- a/src/Pure/PIDE/document_status.scala	Mon Sep 15 17:42:09 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Sep 15 18:09:55 2025 +0200
@@ -18,11 +18,15 @@
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
-    def make(markups: Iterable[Markup]): Command_Status = {
+    def make(
+      markups: Iterable[Markup],
+      warned: Boolean = false,
+      failed: Boolean = false
+    ): Command_Status = {
       var touched = false
       var accepted = false
-      var warned = false
-      var failed = false
+      var warned1 = warned
+      var failed1 = failed
       var canceled = false
       var finalized = false
       var forks = 0
@@ -34,8 +38,8 @@
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
-          case Markup.WARNING | Markup.LEGACY => warned = true
-          case Markup.FAILED | Markup.ERROR => failed = true
+          case Markup.WARNING | Markup.LEGACY => warned1 = true
+          case Markup.FAILED | Markup.ERROR => failed1 = true
           case Markup.CANCELED => canceled = true
           case Markup.FINALIZED => finalized = true
           case _ =>
@@ -44,8 +48,8 @@
       new Command_Status(
         touched = touched,
         accepted = accepted,
-        warned = warned,
-        failed = failed,
+        warned = warned1,
+        failed = failed1,
         canceled = canceled,
         finalized = finalized,
         forks = forks,