src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Fri Feb 14 20:58:48 2014 +0100
+++ b/src/Pure/General/symbol.scala	Fri Feb 14 21:06:20 2014 +0100
@@ -19,9 +19,16 @@
   /* 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_hex(c: Char): Boolean =
+    '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
+
   def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
 
+  def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c)
+
   def is_ascii_letdig(c: Char): Boolean =
     is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)