tuned signature;
authorwenzelm
Mon, 12 Mar 2018 16:39:58 +0100
changeset 67840 a9d450fc5a49
parent 67839 0c2ed45ece20
child 67841 8ada8f6d9495
tuned signature; tuned output;
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 {