# HG changeset patch
# User wenzelm
# Date 1520606634 -3600
# Node ID 8f5f5fbe291b2e597450afd776aae4e629c57139
# Parent  fd30e767d9008dc836715b389d47c3043f9ef03e
added Reply.NOTE for asynchronous notifications;

diff -r fd30e767d900 -r 8f5f5fbe291b src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 15:36:27 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 15:43:54 2018 +0100
@@ -31,7 +31,7 @@
 
   object Reply extends Enumeration
   {
-    val OK, ERROR = Value
+    val OK, ERROR, NOTE = Value
 
     def unapply(line: String): Option[(Reply.Value, JSON.T)] =
     {
@@ -90,6 +90,10 @@
     def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
     def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
       reply_error(Map("message" -> message) ++ more)
+
+    def notify(t: JSON.T) { reply(Server.Reply.NOTE, t) }
+    def notify_message(message: String, more: (String, JSON.T)*): Unit =
+      notify(Map("message" -> message) ++ more)
   }
 
 
@@ -258,7 +262,9 @@
         while (!finished) {
           connection.read_line() match {
             case None => finished = true
-            case Some(line) if line != "" =>
+            case Some("") =>
+              connection.notify_message("Command 'help' provides list of commands")
+            case Some(line) =>
               val (cmd, input) = Server.split_line(line)
               Server.commands.get(cmd) match {
                 case None => connection.reply_error("Bad command " + quote(cmd))
@@ -278,7 +284,6 @@
                         "Malformed command-line", "command" -> cmd, "input" -> input)
                   }
               }
-            case _ =>
           }
         }
       case _ =>