# HG changeset patch
# User wenzelm
# Date 1521479617 -3600
# Node ID 6e85d866251f38644ea6ee266d4bdf65601f1791
# Parent  c88044b10bbfc0cd8a4465505bf19b253ae4d824
clarified message name: disallow single quote;

diff -r c88044b10bbf -r 6e85d866251f src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Mar 18 12:26:30 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 19 18:13:37 2018 +0100
@@ -30,10 +30,12 @@
 
   object Argument
   {
+    def is_name_char(c: Char): Boolean =
+      Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
+
     def split(msg: String): (String, String) =
     {
-      val name =
-        msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
+      val name = msg.takeWhile(is_name_char(_))
       val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
       (name, argument)
     }