1.1 --- a/src/Pure/General/symbol.scala	Thu Jun 16 23:35:37 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Jun 17 00:10:39 2011 +0200
     1.3 @@ -28,6 +28,19 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* ASCII characters */
     1.8 +
     1.9 +  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
    1.10 +  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
    1.11 +  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
    1.12 +
    1.13 +  def is_ascii_letdig(c: Char): Boolean =
    1.14 +    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
    1.15 +
    1.16 +  def is_ascii_identifier(s: String): Boolean =
    1.17 +    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
    1.18 +
    1.19 +
    1.20    /* Symbol regexps */
    1.21  
    1.22    private val plain = new Regex("""(?xs)