some concrete commands;
authorwenzelm
Fri Oct 27 17:06:30 2017 +0200 (19 months ago)
changeset 66929c19b17b72777
parent 66928 33f9133bed7c
child 66930 d4f7c6f14fa2
some concrete commands;
clarified messages;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Fri Oct 27 17:04:41 2017 +0200
     1.2 +++ b/src/Pure/Tools/server.scala	Fri Oct 27 17:06:30 2017 +0200
     1.3 @@ -16,6 +16,11 @@
     1.4  {
     1.5    /* protocol */
     1.6  
     1.7 +  val commands: Map[String, PartialFunction[JSON.T, JSON.T]] =
     1.8 +    Map(
     1.9 +      "help" -> { case JSON.empty => commands.keySet.toList.sorted },
    1.10 +      "echo" -> { case t => t })
    1.11 +
    1.12    object Reply extends Enumeration
    1.13    {
    1.14      val OK, ERROR = Value
    1.15 @@ -152,9 +157,6 @@
    1.16      val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
    1.17      val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
    1.18  
    1.19 -    val Blank_Line = """^\s*$""".r
    1.20 -    val Command_Line = """^(\S+)\s*(.*)$""".r
    1.21 -
    1.22      def reply_line(msg: String)
    1.23      {
    1.24        require(split_lines(msg).length <= 1)
    1.25 @@ -170,6 +172,10 @@
    1.26  
    1.27      def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
    1.28      def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
    1.29 +    def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
    1.30 +      reply_error(Map("message" -> message) ++ more)
    1.31 +
    1.32 +    val Command_Line = """^(\S+)\s*(.*)$""".r
    1.33  
    1.34      reader.readLine() match {
    1.35        case null =>
    1.36 @@ -179,14 +185,24 @@
    1.37          while (!finished) {
    1.38            reader.readLine() match {
    1.39              case null => finished = true
    1.40 -            case Blank_Line() =>
    1.41 -            case Command_Line(cmd, arg) =>
    1.42 -              proper_string(arg) getOrElse "{}" match {
    1.43 -                case JSON.Format(json) =>
    1.44 -                  reply_ok(Map("command" -> cmd, "argument" -> json))
    1.45 -                case _ =>
    1.46 -                  reply_error(
    1.47 -                    Map("message" -> "Malformed command", "command" -> cmd, "input" -> arg))
    1.48 +            case Command_Line(cmd, input) =>
    1.49 +              Server.commands.get(cmd) match {
    1.50 +                case None => reply_error("Unknown command " + quote(cmd))
    1.51 +                case Some(body) =>
    1.52 +                  proper_string(input) getOrElse "{}" match {
    1.53 +                    case JSON.Format(arg) =>
    1.54 +                      if (body.isDefinedAt(arg)) {
    1.55 +                        try { reply_ok(body(arg)) }
    1.56 +                        catch { case ERROR(msg) => reply_error(msg) }
    1.57 +                      }
    1.58 +                      else {
    1.59 +                        reply_error_message(
    1.60 +                          "Bad argument for command", "command" -> cmd, "argument" -> arg)
    1.61 +                      }
    1.62 +                    case _ =>
    1.63 +                      reply_error_message(
    1.64 +                        "Malformed command-line", "command" -> cmd, "input" -> input)
    1.65 +                  }
    1.66                }
    1.67              case _ =>
    1.68            }