equal
deleted
inserted
replaced
51 def is_ascii_letdig(c: Char): Boolean = |
51 def is_ascii_letdig(c: Char): Boolean = |
52 is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c) |
52 is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c) |
53 |
53 |
54 def is_ascii_identifier(s: String): Boolean = |
54 def is_ascii_identifier(s: String): Boolean = |
55 s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) |
55 s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) |
|
56 |
|
57 def ascii(c: Char): Symbol = |
|
58 { |
|
59 if (c > 127) error("Non-ASCII character: " + quote(c.toString)) |
|
60 else char_symbols(c.toInt) |
|
61 } |
56 |
62 |
57 |
63 |
58 /* symbol matching */ |
64 /* symbol matching */ |
59 |
65 |
60 private val symbol_total = new Regex("""(?xs) |
66 private val symbol_total = new Regex("""(?xs) |