tuned signature;
authorwenzelm
Mon Jul 09 23:12:38 2007 +0200 (2007-07-09)
changeset 23674c7cbab93f1d9
parent 23673 67c748e5ae54
child 23675 2d618c190466
tuned signature;
nested source: error msg passed to recover;
src/Pure/General/scan.ML
     1.1 --- a/src/Pure/General/scan.ML	Mon Jul 09 23:12:37 2007 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Mon Jul 09 23:12:38 2007 +0200
     1.3 @@ -60,21 +60,18 @@
     1.4    val trace': ('a * 'b list -> 'c * ('d * 'e list)) -> 'a * 'b list ->
     1.5      ('c * 'b list) * ('d * 'e list)
     1.6    val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
     1.7 -  val try: ('a -> 'b) -> 'a -> 'b
     1.8 -  val force: ('a -> 'b) -> 'a -> 'b
     1.9    val prompt: string -> ('a -> 'b) -> 'a -> 'b
    1.10    val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    1.11      -> 'b * 'a list -> 'c * ('d * 'a list)
    1.12    val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    1.13    val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    1.14 -  val catch: ('a -> 'b) -> 'a -> 'b
    1.15    val error: ('a -> 'b) -> 'a -> 'b
    1.16    val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    1.17      'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    1.18 -    ('d * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
    1.19 +    (string -> 'd * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
    1.20    val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    1.21      'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    1.22 -    ('b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
    1.23 +    (string -> 'b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
    1.24    val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.25    val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.26    type lexicon
    1.27 @@ -213,8 +210,8 @@
    1.28  (* exception handling *)
    1.29  
    1.30  fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    1.31 -fun try scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    1.32 -fun force scan xs = scan xs handle MORE _ => raise FAIL NONE;
    1.33 +fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    1.34 +fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    1.35  fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    1.36  fun catch scan xs = scan xs handle ABORT msg => raise FAIL (SOME msg);
    1.37  fun error scan xs = scan xs handle ABORT msg => Library.error msg;
    1.38 @@ -233,7 +230,7 @@
    1.39    in
    1.40      if exists is_stopper input then
    1.41        raise ABORT "Stopper may not occur in input of finite scan!"
    1.42 -    else (force scan --| lift stop) (state, input @ [stopper])
    1.43 +    else (strict scan --| lift stop) (state, input @ [stopper])
    1.44    end;
    1.45  
    1.46  fun finite stopper scan = unlift (finite' stopper (lift scan));
    1.47 @@ -258,20 +255,21 @@
    1.48  
    1.49      fun drain_loop recover inp =
    1.50        drain_with (catch scanner) inp handle FAIL msg =>
    1.51 -        (Output.error_msg (the_default "Syntax error." msg); drain_with recover inp);
    1.52 +        (drain_with (recover (the_default "Syntax error." msg)) inp);
    1.53  
    1.54      val ((ys, (state', xs')), src') =
    1.55        (case (get def_prmpt src, opt_recover) of
    1.56          (([], s), _) => (([], (state, [])), s)
    1.57        | ((xs, s), NONE) => drain_with (error scanner) ((state, xs), s)
    1.58 -      | ((xs, s), SOME r) => drain_loop (unless (lift (one (#2 stopper))) r) ((state, xs), s));
    1.59 +      | ((xs, s), SOME r) => drain_loop (unless (lift (one (#2 stopper))) o r) ((state, xs), s));
    1.60    in (ys, (state', unget (xs', src'))) end;
    1.61  
    1.62  fun source def_prmpt get unget stopper scan opt_recover =
    1.63 -  unlift (source' def_prmpt get unget stopper (lift scan) (Option.map lift opt_recover));
    1.64 +  unlift (source' def_prmpt get unget stopper (lift scan)
    1.65 +    (Option.map (fn r => lift o r) opt_recover));
    1.66  
    1.67  fun single scan = scan >> (fn x => [x]);
    1.68 -fun bulk scan = scan -- repeat (try scan) >> (op ::);
    1.69 +fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
    1.70  
    1.71  
    1.72