src/Pure/Tools/server.scala
changeset 67903 6e85d866251f
parent 67902 c88044b10bbf
child 67904 465f43a9f780
equal deleted inserted replaced
67902:c88044b10bbf 67903:6e85d866251f
    28 {
    28 {
    29   /* message argument */
    29   /* message argument */
    30 
    30 
    31   object Argument
    31   object Argument
    32   {
    32   {
       
    33     def is_name_char(c: Char): Boolean =
       
    34       Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
       
    35 
    33     def split(msg: String): (String, String) =
    36     def split(msg: String): (String, String) =
    34     {
    37     {
    35       val name =
    38       val name = msg.takeWhile(is_name_char(_))
    36         msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
       
    37       val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
    39       val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
    38       (name, argument)
    40       (name, argument)
    39     }
    41     }
    40 
    42 
    41     def print(arg: Any): String =
    43     def print(arg: Any): String =