equal
deleted
inserted
replaced
233 in |
233 in |
234 |
234 |
235 val scan_char = |
235 val scan_char = |
236 $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; |
236 $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; |
237 |
237 |
|
238 val recover_char = |
|
239 $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; |
|
240 |
238 val scan_string = |
241 val scan_string = |
239 $$$ "\"" @@@ !!! "missing quote at end of string" |
242 $$$ "\"" @@@ !!! "missing quote at end of string" |
240 ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\""); |
243 ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\""); |
|
244 |
|
245 val recover_string = |
|
246 $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat); |
241 |
247 |
242 end; |
248 end; |
243 |
249 |
244 |
250 |
245 (* scan tokens *) |
251 (* scan tokens *) |
263 scan_typevar >> token TypeVar)); |
269 scan_typevar >> token TypeVar)); |
264 |
270 |
265 val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text; |
271 val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text; |
266 |
272 |
267 fun recover msg = |
273 fun recover msg = |
268 Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o Symbol_Pos.symbol) |
274 (recover_char || |
269 >> (fn cs => [token (Error msg) cs]); |
275 recover_string || |
|
276 Symbol_Pos.recover_comment || |
|
277 Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) |
|
278 >> (single o token (Error msg)); |
270 |
279 |
271 in |
280 in |
272 |
281 |
273 fun source src = |
282 fun source src = |
274 Symbol_Pos.source (Position.line 1) src |
283 Symbol_Pos.source (Position.line 1) src |