# HG changeset patch
# User wenzelm
# Date 1520869198 -3600
# Node ID a9d450fc5a4908ad871d2e57faea1e322bcc75b2
# Parent  0c2ed45ece2028fb152f811cbd09e6e1e64adda5
tuned signature;
tuned output;

diff -r 0c2ed45ece20 -r a9d450fc5a49 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Mar 12 16:32:33 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 12 16:39:58 2018 +0100
@@ -155,8 +155,6 @@
       reply_error(Map("message" -> message) ++ more)
 
     def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
-    def notify_message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
-      notify(Map(Markup.KIND -> kind, "message" -> msg) ++ more)
   }
 
 
@@ -168,8 +166,9 @@
 
     def shutdown() { server.close() }
 
+    def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
-      connection.notify_message(kind, msg, more:_*)
+      notify(Map(Markup.KIND -> kind, "message" -> msg) ++ more)
     def writeln(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WRITELN, msg, more:_*)
     def warning(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WARNING, msg, more:_*)
     def error_message(msg: String, more: (String, JSON.T)*): Unit =
@@ -398,7 +397,7 @@
         while (!finished) {
           connection.read_message() match {
             case None => finished = true
-            case Some("") => context.writeln("Command 'help' provides list of commands")
+            case Some("") => context.notify("Command 'help' provides list of commands")
             case Some(msg) =>
               val (name, argument) = Server.Argument.split(msg)
               name match {