# HG changeset patch
# User wenzelm
# Date 1693320128 -7200
# Node ID afb83ba8d24c0f95b7549cfe9ff43ff756427e9d
# Parent  1ce1abed508255a57bb0906c0e84554ce615a68b
clarified signature: prefer enum types;

diff -r 1ce1abed5082 -r afb83ba8d24c src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Aug 29 16:39:29 2023 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Aug 29 16:42:08 2023 +0200
@@ -230,9 +230,7 @@
 
   /* nodes status */
 
-  object Overall_Node_Status extends Enumeration {
-    val ok, failed, pending = Value
-  }
+  enum Overall_Node_Status { case ok, failed, pending }
 
   object Nodes_Status {
     val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
@@ -259,7 +257,7 @@
         case None => false
       }
 
-    def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
+    def overall_node_status(name: Document.Node.Name): Overall_Node_Status =
       rep.get(name) match {
         case Some(st) if st.consolidated =>
           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
diff -r 1ce1abed5082 -r afb83ba8d24c src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Tue Aug 29 16:39:29 2023 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Tue Aug 29 16:42:08 2023 +0200
@@ -30,9 +30,7 @@
   private def is_loaded_theory(name: Document.Node.Name): Boolean =
     PIDE.resources.session_base.loaded_theory(name)
 
-  private def overall_node_status(
-    name: Document.Node.Name
-  ): Document_Status.Overall_Node_Status.Value = {
+  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)
   }