equal
deleted
inserted
replaced
141 local |
141 local |
142 |
142 |
143 val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"]; |
143 val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"]; |
144 |
144 |
145 val scan_delim_char = |
145 val scan_delim_char = |
146 $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) || |
146 $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) || |
147 Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular); |
147 Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); |
148 |
148 |
149 fun read_int ["0", "0"] = ~1 |
149 fun read_int ["0", "0"] = ~1 |
150 | read_int cs = #1 (Library.read_int cs); |
150 | read_int cs = #1 (Library.read_int cs); |
151 |
151 |
152 val scan_sym = |
152 val scan_sym = |