allow "." in message name;

--- a/src/Pure/Tools/server.scala	Mon Mar 12 11:31:39 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 12 11:37:30 2018 +0100
@@ -32,7 +32,8 @@
   {
     def split(msg: String): (String, String) =
     {
-      val name = msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c))
+      val name =
+        msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
       val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
       (name, argument)
     }