more formal messages;
authorwenzelm
Fri Oct 27 16:21:58 2017 +0200 (19 months ago)
changeset 66927153d7b68e8f8
parent 66926 4cf560a6dd84
child 66928 33f9133bed7c
more formal messages;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Fri Oct 27 16:21:29 2017 +0200
     1.2 +++ b/src/Pure/Tools/server.scala	Fri Oct 27 16:21:58 2017 +0200
     1.3 @@ -14,6 +14,14 @@
     1.4  
     1.5  object Server
     1.6  {
     1.7 +  /* protocol */
     1.8 +
     1.9 +  object Reply extends Enumeration
    1.10 +  {
    1.11 +    val OK, ERROR = Value
    1.12 +  }
    1.13 +
    1.14 +
    1.15    /* per-user servers */
    1.16  
    1.17    object Data
    1.18 @@ -147,19 +155,25 @@
    1.19      val Blank_Line = """^\s*$""".r
    1.20      val Command_Line = """^(\S+)\s*(.*)$""".r
    1.21  
    1.22 -    def println(s: String)
    1.23 +    def reply_line(msg: String)
    1.24      {
    1.25 -      writer.write(s)
    1.26 +      require(split_lines(msg).length <= 1)
    1.27 +      writer.write(msg)
    1.28        writer.newLine()
    1.29        writer.flush()
    1.30      }
    1.31  
    1.32 -    def println_result(t: JSON.T) { println("RESULT " + JSON.Format(t)) }
    1.33 -    def println_error(t: JSON.T) { println("ERROR " + JSON.Format(t)) }
    1.34 +    def reply(r: Server.Reply.Value, t: JSON.T)
    1.35 +    {
    1.36 +      reply_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t))
    1.37 +    }
    1.38 +
    1.39 +    def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
    1.40 +    def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
    1.41  
    1.42      reader.readLine() match {
    1.43        case null =>
    1.44 -      case bad if bad != password => println_error("Bad password -- connection closed")
    1.45 +      case bad if bad != password => reply_error("Bad password -- connection closed")
    1.46        case _ =>
    1.47          var finished = false
    1.48          while (!finished) {
    1.49 @@ -169,10 +183,10 @@
    1.50              case Command_Line(cmd, arg) =>
    1.51                proper_string(arg) getOrElse "{}" match {
    1.52                  case JSON.Format(json) =>
    1.53 -                  println_result(Map("command" -> cmd, "argument" -> arg))
    1.54 +                  reply_ok(Map("command" -> cmd, "argument" -> json))
    1.55                  case _ =>
    1.56 -                  println_error(
    1.57 -                    Map("message" -> "Malformed command", "command" -> cmd, "argument" -> arg))
    1.58 +                  reply_error(
    1.59 +                    Map("message" -> "Malformed command", "command" -> cmd, "input" -> arg))
    1.60                }
    1.61              case _ =>
    1.62            }