equal
deleted
inserted
replaced
93 "^" ~ one(character(c => '@' <= c && c <= '_')) ^^ { case x ~ y => x + y } | |
93 "^" ~ one(character(c => '@' <= c && c <= '_')) ^^ { case x ~ y => x + y } | |
94 repeated(character(Symbol.is_ascii_digit), 3, 3) |
94 repeated(character(Symbol.is_ascii_digit), 3, 3) |
95 |
95 |
96 private val str = |
96 private val str = |
97 one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) | |
97 one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) | |
98 one(s => Symbol.is_symbolic(s) | Symbol.is_control(s)) | |
98 one(s => |
|
99 Symbol.is_open(s) || Symbol.is_close(s) || Symbol.is_symbolic(s) || Symbol.is_control(s)) | |
99 "\\" ~ escape ^^ { case x ~ y => x + y } |
100 "\\" ~ escape ^^ { case x ~ y => x + y } |
100 |
101 |
101 |
102 |
102 /* ML char -- without gaps */ |
103 /* ML char -- without gaps */ |
103 |
104 |