# HG changeset patch # User wenzelm # Date 1520777294 -3600 # Node ID e30d6368c7c8555f7e397ddeb904dae1d43b88ab # Parent b73d8ed73b35692f6a24f06d4f1cd5538b15ad34 clarified argument formats: explicit Unit, allow XML.Elem as well; tuned messages: prefer single quotes for JSON output; diff -r b73d8ed73b35 -r e30d6368c7c8 src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Sun Mar 11 15:06:48 2018 +0100 +++ b/src/Pure/PIDE/yxml.scala Sun Mar 11 15:08:14 2018 +0100 @@ -23,8 +23,10 @@ val X_string = X.toString val Y_string = Y.toString + val XY_string = X_string + Y_string def detect(s: String): Boolean = s.exists(c => c == X || c == Y) + def detect_elem(s: String): Boolean = s.startsWith(XY_string) /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) @@ -116,7 +118,13 @@ parse_body(source) match { case List(result) => result case Nil => XML.Text("") - case _ => err("multiple results") + case _ => err("multiple XML trees") + } + + def parse_elem(source: CharSequence): XML.Tree = + parse_body(source) match { + case List(elem: XML.Elem) => elem + case _ => err("single XML element expected") } diff -r b73d8ed73b35 -r e30d6368c7c8 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Sun Mar 11 15:06:48 2018 +0100 +++ b/src/Pure/Tools/server.scala Sun Mar 11 15:08:14 2018 +0100 @@ -4,13 +4,16 @@ Resident Isabelle servers. Message formats: - - short message (single line): NAME ARGUMENT - - long message (multiple lines): BYTE_LENGTH NAME ARGUMENT + +Argument formats: + - Unit as empty string + - XML.Elem in YXML notation + - JSON.T in standard notation */ package isabelle @@ -23,35 +26,68 @@ object Server { - /* protocol */ + /* message argument */ - def split_message(msg: String): (String, String) = + object Argument { - val head = msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c)) - val rest = msg.substring(head.length).dropWhile(Symbol.is_ascii_blank(_)) - (head, proper_string(rest) getOrElse "{}") + def split(msg: String): (String, String) = + { + val name = msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c)) + val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_)) + (name, argument) + } + + def print(arg: Any): String = + arg match { + case () => "" + case t: XML.Elem => YXML.string_of_tree(t) + case t: JSON.T => JSON.Format(t) + } + + def parse(argument: String): Any = + if (argument == "") () + else if (YXML.detect_elem(argument)) YXML.parse_elem(argument) + else JSON.parse(argument, strict = false) + + def unapply(argument: String): Option[Any] = + try { Some(parse(argument)) } + catch { case ERROR(_) => None } } - val commands: Map[String, PartialFunction[(Server, JSON.T), JSON.T]] = - Map( - "echo" -> { case (_, t) => t }, - "help" -> { case (_, JSON.empty) => commands.keySet.toList.sorted }, - "shutdown" -> { case (server, JSON.empty) => server.close(); JSON.empty }) + + /* input command */ + + object Command + { + type T = PartialFunction[(Server, Any), Any] + + private val table: Map[String, T] = + Map( + "echo" -> { case (_, t) => t }, + "help" -> { case (_, ()) => table.keySet.toList.sorted }, + "shutdown" -> { case (server, ()) => server.close(); () }) + + def unapply(name: String): Option[T] = table.get(name) + } + + + /* output reply */ object Reply extends Enumeration { val OK, ERROR, NOTE = Value - def unapply(msg: String): Option[(Reply.Value, JSON.T)] = + def unapply(msg: String): Option[(Reply.Value, Any)] = { if (msg == "") None else { - val (reply, output) = split_message(msg) - try { Some((withName(reply), JSON.parse(output, strict = false))) } - catch { - case _: NoSuchElementException => None - case Exn.ERROR(_) => None - } + val (name, argument) = Argument.split(msg) + for { + reply <- + try { Some(withName(name)) } + catch { case _: NoSuchElementException => None } + arg <- Argument.unapply(argument) + } yield (reply, arg) } } } @@ -96,17 +132,18 @@ try { out.flush() } catch { case _: SocketException => } } - def reply(r: Server.Reply.Value, t: JSON.T) + def reply(r: Server.Reply.Value, arg: Any) { - write_message(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t)) + val argument = Argument.print(arg) + write_message(if (argument == "") r.toString else r.toString + " " + argument) } - def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) } - def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) } + def reply_ok(arg: Any) { reply(Server.Reply.OK, arg) } + def reply_error(arg: Any) { reply(Server.Reply.ERROR, arg) } 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(arg: Any) { reply(Server.Reply.NOTE, arg) } def notify_message(message: String, more: (String, JSON.T)*): Unit = notify(Map("message" -> message) ++ more) } @@ -305,7 +342,7 @@ { connection.read_message() match { case Some(msg) if msg == password => - connection.reply_ok(JSON.empty) + connection.reply_ok(()) var finished = false while (!finished) { connection.read_message() match { @@ -313,24 +350,29 @@ case Some("") => connection.notify_message("Command 'help' provides list of commands") case Some(msg) => - val (cmd, input) = Server.split_message(msg) - Server.commands.get(cmd) match { - case None => connection.reply_error("Bad command " + quote(cmd)) - case Some(body) => - input match { - case JSON.Format(arg) => - if (body.isDefinedAt((server, arg))) { - try { connection.reply_ok(body(server, arg)) } - catch { case ERROR(msg) => connection.reply_error(msg) } + val (name, argument) = Server.Argument.split(msg) + name match { + case Server.Command(cmd) => + argument match { + case Server.Argument(arg) => + if (cmd.isDefinedAt((server, arg))) { + Exn.capture { cmd((server, arg)) } match { + case Exn.Res(res) => connection.reply_ok(res) + case Exn.Exn(ERROR(msg)) => connection.reply_error(msg) + case Exn.Exn(exn) => throw exn + } } else { connection.reply_error_message( - "Bad argument for command", "command" -> cmd, "argument" -> arg) + "Bad argument for command " + Library.single_quote(name), + "argument" -> argument) } case _ => connection.reply_error_message( - "Malformed message", "command" -> cmd, "input" -> input) + "Malformed argument for command " + Library.single_quote(name), + "argument" -> argument) } + case _ => connection.reply_error("Bad command " + Library.single_quote(name)) } } } diff -r b73d8ed73b35 -r e30d6368c7c8 src/Pure/library.scala --- a/src/Pure/library.scala Sun Mar 11 15:06:48 2018 +0100 +++ b/src/Pure/library.scala Sun Mar 11 15:08:14 2018 +0100 @@ -150,6 +150,8 @@ /* quote */ + def single_quote(s: String): String = "'" + s + "'" + def quote(s: String): String = "\"" + s + "\"" def try_unquote(s: String): Option[String] =