moved source cascading from scan.ML to source.ML;
authorwenzelm
Tue Jul 10 16:45:03 2007 +0200 (2007-07-10)
changeset 23700fb1102e98cd4
parent 23699 5a4527f3ac79
child 23701 1716f19e7d25
moved source cascading from scan.ML to source.ML;
src/Pure/General/source.ML
     1.1 --- a/src/Pure/General/source.ML	Tue Jul 10 16:45:01 2007 +0200
     1.2 +++ b/src/Pure/General/source.ML	Tue Jul 10 16:45:03 2007 +0200
     1.3 @@ -136,24 +136,38 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** compose sources **)
     1.8 -
     1.9 -fun drain_source source stopper scan recover prompt src =
    1.10 -  source prompt get_prompt unget stopper scan recover src;
    1.11 -
    1.12 +(** cascade sources **)
    1.13  
    1.14  (* state-based *)
    1.15  
    1.16 +fun drain_source' stopper scan opt_recover prompt (state, src) =
    1.17 +  let
    1.18 +    val drain = Scan.drain prompt get_prompt stopper;
    1.19 +    val (xs, s) = get_prompt prompt src;
    1.20 +    val inp = ((state, xs), s);
    1.21 +    val ((ys, (state', xs')), src') =
    1.22 +      if null xs then (([], (state, [])), s)
    1.23 +      else
    1.24 +        (case opt_recover of
    1.25 +          NONE => drain (Scan.error scan) inp
    1.26 +        | SOME (interactive, recover) =>
    1.27 +            (drain (Scan.catch scan) inp handle Fail msg =>
    1.28 +              (if interactive then Output.error_msg msg else ();
    1.29 +                drain (Scan.unless (Scan.lift (Scan.one (#2 stopper))) (recover msg)) inp)));
    1.30 +  in (ys, (state', unget (xs', src'))) end;
    1.31 +
    1.32  fun source' init_state stopper scan recover src =
    1.33 -  make_source [] (init_state, src) default_prompt
    1.34 -    (drain_source Scan.source' stopper scan recover);
    1.35 +  make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover);
    1.36  
    1.37  
    1.38  (* non state-based *)
    1.39  
    1.40 +fun drain_source stopper scan opt_recover prompt =
    1.41 +  Scan.unlift (drain_source' stopper (Scan.lift scan)
    1.42 +    (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt);
    1.43 +
    1.44  fun source stopper scan recover src =
    1.45 -  make_source [] src default_prompt
    1.46 -    (drain_source Scan.source stopper scan recover);
    1.47 +  make_source [] src default_prompt (drain_source stopper scan recover);
    1.48  
    1.49  
    1.50  end;