--- a/src/Pure/PIDE/document_status.scala Tue Sep 16 12:02:41 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala Tue Sep 16 12:06:07 2025 +0200
@@ -142,17 +142,7 @@
/* node status */
object Node_Status {
- val empty: Node_Status =
- Node_Status(
- suppressed = false,
- unprocessed = 0,
- running = 0,
- warned = 0,
- failed = 0,
- finished = 0,
- canceled = false,
- terminated = false,
- theory_status = Document_Status.Theory_Status.NONE)
+ val empty: Node_Status = Node_Status()
def make(
state: Document.State,
@@ -198,15 +188,15 @@
}
sealed case class Node_Status(
- suppressed: Boolean,
- unprocessed: Int,
- running: Int,
- warned: Int,
- failed: Int,
- finished: Int,
- canceled: Boolean,
- terminated: Boolean,
- theory_status: Theory_Status.Value
+ suppressed: Boolean = false,
+ unprocessed: Int = 0,
+ running: Int = 0,
+ warned: Int = 0,
+ failed: Int = 0,
+ finished: Int = 0,
+ canceled: Boolean = false,
+ terminated: Boolean = false,
+ theory_status: Theory_Status.Value = Theory_Status.NONE
) extends Theory_Status {
def is_empty: Boolean = this == Node_Status.empty