equal
deleted
inserted
replaced
55 def is_ascii_identifier(s: String): Boolean = |
55 def is_ascii_identifier(s: String): Boolean = |
56 s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) |
56 s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) |
57 |
57 |
58 def ascii(c: Char): Symbol = |
58 def ascii(c: Char): Symbol = |
59 { |
59 { |
60 if (c > 127) error("Non-ASCII character: " + XLibrary.quote(c.toString)) |
60 if (c > 127) { |
|
61 Console.printf("Non-ASCII character: " + XLibrary.quote(c.toString)); |
|
62 "Non-ASCII character: " + XLibrary.quote(c.toString) |
|
63 } |
61 else char_symbols(c.toInt) |
64 else char_symbols(c.toInt) |
62 } |
65 } |
63 |
66 |
64 |
67 |
65 /* symbol matching */ |
68 /* symbol matching */ |