# HG changeset patch
# User wenzelm
# Date 1758102087 -7200
# Node ID 47edc6384e7aa97facd40209ffe7e6ae1b4bd980
# Parent  9e05d3acd2b4db41eb548e4da2542e73be0ac028
tuned signature: more explicit operations;

diff -r 9e05d3acd2b4 -r 47edc6384e7a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Sep 17 11:30:59 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 17 11:41:27 2025 +0200
@@ -259,8 +259,7 @@
     }
 
     private def add_status(st: Markup): State = {
-      val document_status1 =
-        document_status + Document_Status.Command_Status.make(markups = List(st))
+      val document_status1 = document_status.update(markups = List(st))
       new State(command, st :: status, results, exports, markups, document_status1)
     }
 
diff -r 9e05d3acd2b4 -r 47edc6384e7a src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Wed Sep 17 11:30:59 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 17 11:41:27 2025 +0200
@@ -41,7 +41,7 @@
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
     def make(
-      markups: Iterable[Markup] = Nil,
+      markups: List[Markup] = Nil,
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
@@ -127,22 +127,28 @@
           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 update(
+      markups: List[Markup] = Nil,
+      warned: Boolean = false,
+      failed: Boolean = false
+    ): Command_Status = {
+      if (markups.isEmpty) {
+        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)
+        }
       }
+      else this + Command_Status.make(markups = markups, warned = warned, failed = failed)
     }
 
     def maybe_consolidated: Boolean = touched && forks == 0 && runs == 0