clarified signature;

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 12:14:37 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 12:24:12 2025 +0200
@@ -260,7 +260,7 @@
 
   /* nodes status */
 
-  enum Overall_Node_Status { case ok, failed, pending }
+  enum Overall_Status { case ok, failed, pending }
 
   object Nodes_Status {
     val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
@@ -287,11 +287,11 @@
         case None => false
       }
 
-    def overall_node_status(name: Document.Node.Name): Overall_Node_Status =
+    def overall_status(name: Document.Node.Name): Overall_Status =
       rep.get(name) match {
         case Some(st) if st.consolidated =>
-          if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
-        case _ => Overall_Node_Status.pending
+          if (st.ok) Overall_Status.ok else Overall_Status.failed
+        case _ => Overall_Status.pending
       }
 
     def update(
@@ -328,10 +328,10 @@
       var pending = 0
       var canceled = 0
       for (name <- rep.keysIterator) {
-        overall_node_status(name) match {
-          case Overall_Node_Status.ok => ok += 1
-          case Overall_Node_Status.failed => failed += 1
-          case Overall_Node_Status.pending => pending += 1
+        overall_status(name) match {
+          case Overall_Status.ok => ok += 1
+          case Overall_Status.failed => failed += 1
+          case Overall_Status.pending => pending += 1
         }
         if (apply(name).canceled) canceled += 1
       }

--- a/src/Tools/jEdit/src/theories_status.scala	Tue Sep 16 12:14:37 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Tue Sep 16 12:24:12 2025 +0200
@@ -28,10 +28,9 @@
   private def is_loaded_theory(name: Document.Node.Name): Boolean =
     PIDE.resources.loaded_theory(name)
 
-  private def overall_node_status(name: Document.Node.Name): Document_Status.Overall_Node_Status = {
-    if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok
-    else nodes_status.overall_node_status(name)
-  }
+  private def overall_status(name: Document.Node.Name): Document_Status.Overall_Status =
+    if (is_loaded_theory(name)) Document_Status.Overall_Status.ok
+    else nodes_status.overall_status(name)
 
   private def init_state(): Unit = GUI_Thread.require {
     if (document) {
@@ -128,16 +127,16 @@
       }
 
       def label_border(name: Document.Node.Name): Unit = {
-        val st = overall_node_status(name)
+        val st = overall_status(name)
         val color =
           st match {
-            case Document_Status.Overall_Node_Status.ok =>
+            case Document_Status.Overall_Status.ok =>
               PIDE.options.color_value("ok_color")
-            case Document_Status.Overall_Node_Status.failed =>
+            case Document_Status.Overall_Status.failed =>
               PIDE.options.color_value("failed_color")
             case _ => label.foreground
           }
-        val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+        val thickness1 = if (st == Document_Status.Overall_Status.pending) 1 else 3
         val thickness2 = 4 - thickness1
 
         label.border =
@@ -211,10 +210,10 @@
         }
         else if (index >= 0 && node_renderer.in_label(index_location, point)) {
           val name = listData(index)
-          val st = overall_node_status(name)
+          val st = overall_status(name)
           tooltip =
             "theory " + quote(name.theory) +
-              (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
+              (if (st == Document_Status.Overall_Status.ok) "" else " (" + st + ")")
         }
         else tooltip = null
     }