clarified signature;
clarified output;

--- a/src/Pure/PIDE/command.scala	Mon Sep 15 16:57:56 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 15 17:28:22 2025 +0200
@@ -239,7 +239,7 @@
         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).iterator)
+      Document_Status.Command_Status.make(warnings ::: errors ::: status)
     }
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)

--- a/src/Pure/PIDE/document_status.scala	Mon Sep 15 16:57:56 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Sep 15 17:28:22 2025 +0200
@@ -18,7 +18,7 @@
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
-    def make(markup_iterator: Iterator[Markup]): Command_Status = {
+    def make(markups: Iterable[Markup]): Command_Status = {
       var touched = false
       var accepted = false
       var warned = false
@@ -27,7 +27,7 @@
       var finalized = false
       var forks = 0
       var runs = 0
-      for (markup <- markup_iterator) {
+      for (markup <- markups) {
         markup.name match {
           case Markup.ACCEPTED => accepted = true
           case Markup.FORKED => touched = true; forks += 1
@@ -41,7 +41,7 @@
           case _ =>
         }
       }
-      Command_Status(
+      new Command_Status(
         touched = touched,
         accepted = accepted,
         warned = warned,
@@ -52,7 +52,7 @@
         runs = runs)
     }
 
-    val empty: Command_Status = make(Iterator.empty)
+    val empty: Command_Status = make(Nil)
 
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {
@@ -62,18 +62,23 @@
       else empty
   }
 
-  sealed case class Command_Status(
+  final class Command_Status private(
     private val touched: Boolean,
     private val accepted: Boolean,
     private val warned: Boolean,
     private val failed: Boolean,
     private val canceled: Boolean,
     private val finalized: Boolean,
-    forks: Int,
-    runs: Int
+    val forks: Int,
+    val runs: Int
   ) {
+    override def toString: String =
+      if (failed) "Command_Status(failed)"
+      else if (warned) "Command_Status(warned)"
+      else "Command_Status()"
+
     def + (that: Command_Status): Command_Status =
-      Command_Status(
+      new Command_Status(
         touched = touched || that.touched,
         accepted = accepted || that.accepted,
         warned = warned || that.warned,

--- a/src/Pure/PIDE/rendering.scala	Mon Sep 15 16:57:56 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Sep 15 17:28:22 2025 +0200
@@ -510,7 +510,7 @@
       color <-
         result match {
           case (markups, opt_color) if markups.nonEmpty =>
-            val status = Document_Status.Command_Status.make(markups.iterator)
+            val status = Document_Status.Command_Status.make(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)
@@ -778,7 +778,7 @@
             }, status = true)
       if (results.isEmpty) None
       else {
-        val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
+        val status = Document_Status.Command_Status.make(results.flatMap(_.info))
 
         if (status.is_running) Some(Rendering.Color.running)
         else if (status.is_failed) Some(Rendering.Color.error)