clarified signature;
authorwenzelm
Tue, 16 Sep 2025 10:39:53 +0200
changeset 83163 64c9d94478b8
parent 83161 87ceb18f23f3
child 83164 851f3f9440ef
clarified signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/document_status.scala
src/Tools/jEdit/src/theories_status.scala
--- 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
         }
     }