tuned signature: more explicit operations;

--- a/src/Pure/PIDE/command.scala	Tue Sep 16 21:04:39 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 17 11:30:59 2025 +0200
@@ -265,15 +265,10 @@
     }
 
     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)
-        }
+        document_status.update(
+          warned = Results.warned(entry),
+          failed = Results.failed(entry))
       new State(command, status, results + entry, exports, markups, document_status1)
     }
 

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 21:04:39 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 17 11:30:59 2025 +0200
@@ -127,6 +127,24 @@
           runs = runs + that.runs)
       }
 
+    def update(warned: Boolean = false, failed: Boolean = false): Command_Status = {
+      val warned1 = this.warned || warned
+      val failed1 = this.failed || failed
+      if (this.warned == warned1 && this.failed == failed1) this
+      else {
+        new Command_Status(
+          theory_status = theory_status,
+          touched = touched,
+          accepted = accepted,
+          warned = warned1,
+          failed = failed1,
+          canceled = canceled,
+          forks = forks,
+          runs = runs
+        )
+      }
+    }
+
     def maybe_consolidated: Boolean = touched && forks == 0 && runs == 0
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))