src/Pure/Tools/server.scala

     def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
     def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
     def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
       reply_error(Map("message" -> message) ++ more)
 
-    val Command_Line = """^(\S+)\s*(.*)$""".r
-
     reader.readLine() match {
       case null =>
       case bad if bad != password => reply_error("Bad password -- connection closed")
       case _ =>
         var finished = false
         while (!finished) {
           reader.readLine() match {
             case null => finished = true
-            case Command_Line(cmd, input) =>
+            case 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(_))
               Server.commands.get(cmd) match {
-                case None => reply_error("Unknown command " + quote(cmd))
+                case None => reply_error("Bad command " + quote(cmd))
                 case Some(body) =>
                   proper_string(input) getOrElse "{}" match {
                     case JSON.Format(arg) =>
                       if (body.isDefinedAt(arg)) {
                         try { reply_ok(body(arg)) }