# HG changeset patch
# User wenzelm
# Date 1521053907 -3600
# Node ID 612846bff1ea43496eba4b690834946644f37333
# Parent  cba5c565737861fc50fd69bad0c7a6b7769e2b12
tuned signature;

diff -r cba5c5657378 -r 612846bff1ea src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Wed Mar 14 17:43:30 2018 +0100
+++ b/src/Pure/Tools/server.scala	Wed Mar 14 19:58:27 2018 +0100
@@ -152,18 +152,18 @@
       try { out.flush() } catch { case _: SocketException => }
     }
 
-    def reply(r: Server.Reply.Value, arg: Any)
+    def reply(r: Reply.Value, arg: Any)
     {
       val argument = Argument.print(arg)
       write_message(if (argument == "") r.toString else r.toString + " " + argument)
     }
 
-    def reply_ok(arg: Any) { reply(Server.Reply.OK, arg) }
-    def reply_error(arg: Any) { reply(Server.Reply.ERROR, arg) }
+    def reply_ok(arg: Any) { reply(Reply.OK, arg) }
+    def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
     def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
       reply_error(JSON.Object(Reply.message(message)) ++ more)
 
-    def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
+    def notify(arg: Any) { reply(Reply.NOTE, arg) }
   }
 
 
@@ -175,6 +175,7 @@
 
     def shutdown() { server.close() }
 
+    def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
     def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
       notify(JSON.Object(Markup.KIND -> kind, Reply.message(msg)) ++ more)