src/Pure/General/symbol.scala

   {
     require(k >= 0)
     if (k < static_spaces.length) static_spaces.substring(0, k)
     else space * k
   }
+
+
+  /* ASCII characters */
+
+  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
+  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
+  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
+
+  def is_ascii_letdig(c: Char): Boolean =
+    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
+
+  def is_ascii_identifier(s: String): Boolean =
+    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
 
 
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)