250 ([], _) => (finite' stopper scan (state, xs), src) |
250 ([], _) => (finite' stopper scan (state, xs), src) |
251 | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src')); |
251 | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src')); |
252 |
252 |
253 fun source' def_prmpt get unget stopper scanner opt_recover (state, src) = |
253 fun source' def_prmpt get unget stopper scanner opt_recover (state, src) = |
254 let |
254 let |
255 val drain_with = drain def_prmpt get stopper; |
255 val draining = drain def_prmpt get stopper; |
|
256 val (xs, s) = get def_prmpt src; |
|
257 val inp = ((state, xs), s); |
256 val ((ys, (state', xs')), src') = |
258 val ((ys, (state', xs')), src') = |
257 (case (get def_prmpt src, opt_recover) of |
259 if null xs then (([], (state, [])), s) |
258 (([], s), _) => (([], (state, [])), s) |
260 else |
259 | ((xs, s), NONE) => drain_with (error scanner) ((state, xs), s) |
261 (case opt_recover of |
260 | ((xs, s), SOME (interactive, recover)) => |
262 NONE => draining (error scanner) inp |
261 let val inp = ((state, xs), s) in |
263 | SOME (interactive, recover) => |
262 drain_with (catch scanner) inp handle FAIL msg => |
264 (draining (catch scanner) inp handle FAIL msg => |
263 let val err = the_default "Syntax error." msg in |
265 let val err = the_default "Syntax error." msg in |
264 if interactive then Output.error_msg err else (); |
266 if interactive then Output.error_msg err else (); |
265 drain_with (unless (lift (one (#2 stopper))) (recover err)) inp |
267 draining (unless (lift (one (#2 stopper))) (recover err)) inp |
266 end |
268 end)); |
267 end); |
|
268 in (ys, (state', unget (xs', src'))) end; |
269 in (ys, (state', unget (xs', src'))) end; |
269 |
270 |
270 fun source def_prmpt get unget stopper scan opt_recover = |
271 fun source def_prmpt get unget stopper scan opt_recover = |
271 unlift (source' def_prmpt get unget stopper (lift scan) |
272 unlift (source' def_prmpt get unget stopper (lift scan) |
272 (Option.map (fn (int, r) => (int, lift o r)) opt_recover)); |
273 (Option.map (fn (int, r) => (int, lift o r)) opt_recover)); |