# 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)