# HG changeset patch
# User wenzelm
# Date 1693316959 -7200
# Node ID 470d4f1e89d9f3a3b13ef83670832c7f5a5440b7
# Parent  b0abf5a9dada5cd7c48f2d1a30d3914acf3e705a
clarified signature: prefer enum types;

diff -r b0abf5a9dada -r 470d4f1e89d9 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Aug 29 15:34:45 2023 +0200
+++ b/src/Pure/Tools/server.scala	Tue Aug 29 15:49:19 2023 +0200
@@ -91,29 +91,29 @@
       case _ => JSON.Object.empty
     }
 
-  object Reply extends Enumeration {
-    val OK, ERROR, FINISHED, FAILED, NOTE = Value
-
+  object Reply {
     def message(msg: String, kind: String = ""): JSON.Object.T =
       JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
 
     def error_message(msg: String): JSON.Object.T =
       message(msg, kind = Markup.ERROR)
 
-    def unapply(msg: String): Option[(Reply.Value, Any)] = {
+    def unapply(msg: String): Option[(Reply, Any)] = {
       if (msg == "") None
       else {
         val (name, argument) = Argument.split(msg)
         for {
           reply <-
-            try { Some(withName(name)) }
-            catch { case _: NoSuchElementException => None }
+            try { Some(Reply.valueOf(name)) }
+            catch { case _: IllegalArgumentException => None }
           arg <- Argument.unapply(argument)
         } yield (reply, arg)
       }
     }
   }
 
+  enum Reply { case OK, ERROR, FINISHED, FAILED, NOTE }
+
 
   /* handler: port, password, thread */
 
@@ -194,7 +194,7 @@
     def write_byte_message(chunks: List[Bytes]): Unit =
       out_lock.synchronized { Byte_Message.write_message(out, chunks) }
 
-    def reply(r: Reply.Value, arg: Any): Unit = {
+    def reply(r: Reply, arg: Any): Unit = {
       val argument = Argument.print(arg)
       write_line_message(if (argument == "") r.toString else r.toString + " " + argument)
     }
@@ -216,7 +216,7 @@
 
     def command_list: List[String] = command_table.keys.toList.sorted
 
-    def reply(r: Reply.Value, arg: Any): Unit = connection.reply(r, arg)
+    def reply(r: Reply, arg: Any): Unit = connection.reply(r, arg)
     def notify(arg: Any): Unit = connection.notify(arg)
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
       notify(Reply.message(msg, kind = kind) ++ more)