# HG changeset patch
# User wenzelm
# Date 1520539762 -3600
# Node ID 543e36ae489c8d5272d8e66a2ad57bedb2b821aa
# Parent  839de121665c40ba48dbb791c88cf280c22f748e
tuned -- avoid regex matching on potentially large string;
clarified message: command name could be malformed;

diff -r 839de121665c -r 543e36ae489c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 08 14:12:25 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 08 21:09:22 2018 +0100
@@ -175,8 +175,6 @@
     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")
@@ -185,9 +183,11 @@
         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) =>