# HG changeset patch
# User wenzelm
# Date 1520601968 -3600
# Node ID 82c5ca89ac61e1e66a20bff45d48059c885563bf
# Parent  d0eeaeab48cc591bfc077888df7329f6e26d39d3
tuned;

diff -r d0eeaeab48cc -r 82c5ca89ac61 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 13:36:52 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 14:26:08 2018 +0100
@@ -16,6 +16,13 @@
 {
   /* protocol */
 
+  def split_line(line: String): (String, String) =
+  {
+    val head = line.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c))
+    val rest = line.substring(head.length).dropWhile(Symbol.is_ascii_blank(_))
+    (head, proper_string(rest) getOrElse "{}")
+  }
+
   val commands: Map[String, PartialFunction[(Server, JSON.T), JSON.T]] =
     Map(
       "echo" -> { case (_, t) => t },
@@ -224,12 +231,11 @@
           connection.read_line() match {
             case None => finished = true
             case Some(line) =>
-              val cmd = line.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c))
-              val input = line.substring(cmd.length).dropWhile(Symbol.is_ascii_blank(_))
+              val (cmd, input) = Server.split_line(line)
               Server.commands.get(cmd) match {
                 case None => connection.reply_error("Bad command " + quote(cmd))
                 case Some(body) =>
-                  proper_string(input) getOrElse "{}" match {
+                  input match {
                     case JSON.Format(arg) =>
                       if (body.isDefinedAt((server, arg))) {
                         try { connection.reply_ok(body(server, arg)) }