# HG changeset patch
# User wenzelm
# Date 1509114118 -7200
# Node ID 153d7b68e8f82465d2d04b0f9d4377753827d68d
# Parent  4cf560a6dd8492b7fcc8dbcefe853f708c83512d
more formal messages;

diff -r 4cf560a6dd84 -r 153d7b68e8f8 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Oct 27 16:21:29 2017 +0200
+++ b/src/Pure/Tools/server.scala	Fri Oct 27 16:21:58 2017 +0200
@@ -14,6 +14,14 @@
 
 object Server
 {
+  /* protocol */
+
+  object Reply extends Enumeration
+  {
+    val OK, ERROR = Value
+  }
+
+
   /* per-user servers */
 
   object Data
@@ -147,19 +155,25 @@
     val Blank_Line = """^\s*$""".r
     val Command_Line = """^(\S+)\s*(.*)$""".r
 
-    def println(s: String)
+    def reply_line(msg: String)
     {
-      writer.write(s)
+      require(split_lines(msg).length <= 1)
+      writer.write(msg)
       writer.newLine()
       writer.flush()
     }
 
-    def println_result(t: JSON.T) { println("RESULT " + JSON.Format(t)) }
-    def println_error(t: JSON.T) { println("ERROR " + JSON.Format(t)) }
+    def reply(r: Server.Reply.Value, t: JSON.T)
+    {
+      reply_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t))
+    }
+
+    def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
+    def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
 
     reader.readLine() match {
       case null =>
-      case bad if bad != password => println_error("Bad password -- connection closed")
+      case bad if bad != password => reply_error("Bad password -- connection closed")
       case _ =>
         var finished = false
         while (!finished) {
@@ -169,10 +183,10 @@
             case Command_Line(cmd, arg) =>
               proper_string(arg) getOrElse "{}" match {
                 case JSON.Format(json) =>
-                  println_result(Map("command" -> cmd, "argument" -> arg))
+                  reply_ok(Map("command" -> cmd, "argument" -> json))
                 case _ =>
-                  println_error(
-                    Map("message" -> "Malformed command", "command" -> cmd, "argument" -> arg))
+                  reply_error(
+                    Map("message" -> "Malformed command", "command" -> cmd, "input" -> arg))
               }
             case _ =>
           }