# HG changeset patch
# User wenzelm
# Date 1693316085 -7200
# Node ID b0abf5a9dada5cd7c48f2d1a30d3914acf3e705a
# Parent  1cce41dc0c41a138492eb1725561efee340c3ab6
clarified signature: prefer enum types;

diff -r 1cce41dc0c41 -r b0abf5a9dada src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Aug 29 15:23:06 2023 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 29 15:34:45 2023 +0200
@@ -9,11 +9,7 @@
 
 
 object Query_Operation {
-  object Status extends Enumeration {
-    val WAITING = Value("waiting")
-    val RUNNING = Value("running")
-    val FINISHED = Value("finished")
-  }
+  enum Status { case waiting, running, finished }
 
   object State {
     val empty: State = State()
@@ -22,7 +18,7 @@
       State(instance = Document_ID.make().toString,
         location = Some(command),
         query = query,
-        status = Status.WAITING)
+        status = Status.waiting)
   }
 
   sealed case class State(
@@ -31,7 +27,7 @@
     query: List[String] = Nil,
     update_pending: Boolean = false,
     output: List[XML.Tree] = Nil,
-    status: Status.Value = Status.FINISHED,
+    status: Status = Status.finished,
     exec_id: Document_ID.Exec = Document_ID.none)
 }
 
@@ -39,7 +35,7 @@
   editor: Editor[Editor_Context],
   editor_context: Editor_Context,
   operation_name: String,
-  consume_status: Query_Operation.Status.Value => Unit,
+  consume_status: Query_Operation.Status => Unit,
   consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit
 ) {
   private val print_function = operation_name + "_query"
@@ -124,21 +120,20 @@
 
     /* status */
 
-    def get_status(name: String, status: Query_Operation.Status.Value)
-        : Option[Query_Operation.Status.Value] =
+    def get_status(name: String, status: Query_Operation.Status): Option[Query_Operation.Status] =
       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
 
     val new_status =
-      if (removed) Query_Operation.Status.FINISHED
+      if (removed) Query_Operation.Status.finished
       else
-        get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
-        get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
-        Query_Operation.Status.WAITING
+        get_status(Markup.FINISHED, Query_Operation.Status.finished) orElse
+        get_status(Markup.RUNNING, Query_Operation.Status.running) getOrElse
+        Query_Operation.Status.waiting
 
 
     /* state update */
 
-    if (new_status == Query_Operation.Status.RUNNING)
+    if (new_status == Query_Operation.Status.running)
       results.collectFirst(
       {
         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
@@ -157,7 +152,7 @@
         if (state0.status != new_status) {
           current_state.change(_.copy(status = new_status))
           consume_status(new_status)
-          if (new_status == Query_Operation.Status.FINISHED)
+          if (new_status == Query_Operation.Status.finished)
             remove_overlay()
         }
       }
@@ -214,7 +209,7 @@
         state.location match {
           case Some(command)
           if state.update_pending ||
-            (state.status != Query_Operation.Status.FINISHED &&
+            (state.status != Query_Operation.Status.finished &&
               changed.commands.contains(command)) =>
             editor.send_dispatcher { content_update() }
           case _ =>
@@ -230,6 +225,6 @@
     remove_overlay()
     current_state.change(_ => Query_Operation.State.empty)
     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
-    consume_status(Query_Operation.Status.FINISHED)
+    consume_status(Query_Operation.Status.finished)
   }
 }
diff -r 1cce41dc0c41 -r b0abf5a9dada src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue Aug 29 15:23:06 2023 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue Aug 29 15:34:45 2023 +0200
@@ -55,14 +55,14 @@
 
   def consume_status(
     process_indicator: Process_Indicator,
-    status: Query_Operation.Status.Value
+    status: Query_Operation.Status
   ): Unit = {
     status match {
-      case Query_Operation.Status.WAITING =>
+      case Query_Operation.Status.waiting =>
         process_indicator.update("Waiting for evaluation of context ...", 5)
-      case Query_Operation.Status.RUNNING =>
+      case Query_Operation.Status.running =>
         process_indicator.update("Running find operation ...", 15)
-      case Query_Operation.Status.FINISHED =>
+      case Query_Operation.Status.finished =>
         process_indicator.update(null, 0)
     }
   }
diff -r 1cce41dc0c41 -r b0abf5a9dada src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Aug 29 15:23:06 2023 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Aug 29 15:34:45 2023 +0200
@@ -34,13 +34,13 @@
 
   private val process_indicator = new Process_Indicator
 
-  private def consume_status(status: Query_Operation.Status.Value): Unit = {
+  private def consume_status(status: Query_Operation.Status): Unit = {
     status match {
-      case Query_Operation.Status.WAITING =>
+      case Query_Operation.Status.waiting =>
         process_indicator.update("Waiting for evaluation of context ...", 5)
-      case Query_Operation.Status.RUNNING =>
+      case Query_Operation.Status.running =>
         process_indicator.update("Sledgehammering ...", 15)
-      case Query_Operation.Status.FINISHED =>
+      case Query_Operation.Status.finished =>
         process_indicator.update(null, 0)
     }
   }