--- a/src/Pure/PIDE/document.scala Mon Sep 15 23:25:20 2025 +0200
+++ b/src/Pure/PIDE/document.scala Tue Sep 16 10:39:53 2025 +0200
@@ -385,13 +385,13 @@
final class Nodes private(graph: Graph[Node.Name, Node]) {
def apply(name: Node.Name): Node = Nodes.init(graph, name).get_node(name)
- def is_suppressed(name: Node.Name): Boolean = {
+ def suppressed(name: Node.Name): Boolean = {
val graph1 = Nodes.init(graph, name)
graph1.is_maximal(name) && graph1.get_node(name).is_empty
}
def purge_suppressed: Option[Nodes] =
- graph.keys_iterator.filter(is_suppressed).toList match {
+ graph.keys_iterator.filter(suppressed).toList match {
case Nil => None
case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
}
--- a/src/Pure/PIDE/document_status.scala Mon Sep 15 23:25:20 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala Tue Sep 16 10:39:53 2025 +0200
@@ -140,7 +140,7 @@
object Node_Status {
val empty: Node_Status =
Node_Status(
- is_suppressed = false,
+ suppressed = false,
unprocessed = 0,
running = 0,
warned = 0,
@@ -185,7 +185,7 @@
val consolidated = state.node_consolidated(version, name)
Node_Status(
- is_suppressed = version.nodes.is_suppressed(name),
+ suppressed = version.nodes.suppressed(name),
unprocessed = unprocessed,
running = running,
warned = warned,
@@ -200,7 +200,7 @@
}
sealed case class Node_Status(
- is_suppressed: Boolean,
+ suppressed: Boolean,
unprocessed: Int,
running: Int,
warned: Int,
@@ -217,7 +217,7 @@
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
- def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
+ def quasi_consolidated: Boolean = !suppressed && !finalized && terminated
def percentage: Int =
if (consolidated) 100
--- a/src/Tools/jEdit/src/theories_status.scala Mon Sep 15 23:25:20 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Sep 16 10:39:53 2025 +0200
@@ -249,7 +249,7 @@
else {
(for {
(name, node_status) <- nodes_status1.present().iterator
- if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0
+ if !node_status.is_empty && !node_status.suppressed && node_status.total > 0
} yield name).toList
}
}