--- 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))