tuned;
authorwenzelm
Tue Jul 10 00:43:51 2007 +0200 (2007-07-10)
changeset 236831fcfb8682209
parent 23682 cf4773532006
child 23684 8c508c4dc53b
tuned;
src/Pure/General/scan.ML
     1.1 --- a/src/Pure/General/scan.ML	Tue Jul 10 00:17:52 2007 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Tue Jul 10 00:43:51 2007 +0200
     1.3 @@ -252,19 +252,20 @@
     1.4  
     1.5  fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
     1.6    let
     1.7 -    val drain_with = drain def_prmpt get stopper;
     1.8 +    val draining = drain def_prmpt get stopper;
     1.9 +    val (xs, s) = get def_prmpt src;
    1.10 +    val inp = ((state, xs), s);
    1.11      val ((ys, (state', xs')), src') =
    1.12 -      (case (get def_prmpt src, opt_recover) of
    1.13 -        (([], s), _) => (([], (state, [])), s)
    1.14 -      | ((xs, s), NONE) => drain_with (error scanner) ((state, xs), s)
    1.15 -      | ((xs, s), SOME (interactive, recover)) =>
    1.16 -          let val inp = ((state, xs), s) in
    1.17 -            drain_with (catch scanner) inp handle FAIL msg =>
    1.18 +      if null xs then (([], (state, [])), s)
    1.19 +      else
    1.20 +        (case opt_recover of
    1.21 +          NONE => draining (error scanner) inp
    1.22 +        | SOME (interactive, recover) =>
    1.23 +            (draining (catch scanner) inp handle FAIL msg =>
    1.24                let val err = the_default "Syntax error." msg in
    1.25                  if interactive then Output.error_msg err else ();
    1.26 -                drain_with (unless (lift (one (#2 stopper))) (recover err)) inp
    1.27 -              end
    1.28 -          end);
    1.29 +                draining (unless (lift (one (#2 stopper))) (recover err)) inp
    1.30 +              end));
    1.31    in (ys, (state', unget (xs', src'))) end;
    1.32  
    1.33  fun source def_prmpt get unget stopper scan opt_recover =