clarified message name: disallow single quote;
authorwenzelm
Mon Mar 19 18:13:37 2018 +0100 (8 months ago)
changeset 679036e85d866251f
parent 67902 c88044b10bbf
child 67904 465f43a9f780
clarified message name: disallow single quote;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Sun Mar 18 12:26:30 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Mon Mar 19 18:13:37 2018 +0100
     1.3 @@ -30,10 +30,12 @@
     1.4  
     1.5    object Argument
     1.6    {
     1.7 +    def is_name_char(c: Char): Boolean =
     1.8 +      Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
     1.9 +
    1.10      def split(msg: String): (String, String) =
    1.11      {
    1.12 -      val name =
    1.13 -        msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
    1.14 +      val name = msg.takeWhile(is_name_char(_))
    1.15        val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
    1.16        (name, argument)
    1.17      }