src/Pure/General/symbol.scala
changeset 73602 ec52a1a6ed31
parent 73587 0af9e7e4476f
child 73606 d8a0e996614b
equal deleted inserted replaced
73601:79b120d1c1a3 73602:ec52a1a6ed31
    68   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
    68   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
    69 
    69 
    70 
    70 
    71   /* symbol matching */
    71   /* symbol matching */
    72 
    72 
    73   private val symbol_total = new Regex("""(?xs)
    73   private val symbol_total =
    74     [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
    74     new Regex("(?xs) [\ud800-\udbff][\udc00-\udfff] " +
       
    75       """ | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
    75 
    76 
    76   private def is_plain(c: Char): Boolean =
    77   private def is_plain(c: Char): Boolean =
    77     !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
    78     !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
    78 
    79 
    79   def is_malformed(s: Symbol): Boolean =
    80   def is_malformed(s: Symbol): Boolean =