equal
deleted
inserted
replaced
57 def ascii(c: Char): Symbol = |
57 def ascii(c: Char): Symbol = |
58 { |
58 { |
59 if (c > 127) error("Non-ASCII character: " + quote(c.toString)) |
59 if (c > 127) error("Non-ASCII character: " + quote(c.toString)) |
60 else char_symbols(c.toInt) |
60 else char_symbols(c.toInt) |
61 } |
61 } |
|
62 |
|
63 def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128 |
62 |
64 |
63 |
65 |
64 /* symbol matching */ |
66 /* symbol matching */ |
65 |
67 |
66 private val symbol_total = new Regex("""(?xs) |
68 private val symbol_total = new Regex("""(?xs) |