nested source: explicit interactive flag for recover avoids duplicate errors;
authorwenzelm
Tue Jul 10 00:17:52 2007 +0200 (2007-07-10)
changeset 23682cf4773532006
parent 23681 ccf77119dd4d
child 23683 1fcfb8682209
nested source: explicit interactive flag for recover avoids duplicate errors;
src/Pure/General/scan.ML
src/Pure/General/source.ML
src/Pure/General/symbol.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/General/scan.ML	Mon Jul 09 23:12:51 2007 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Tue Jul 10 00:17:52 2007 +0200
     1.3 @@ -68,10 +68,11 @@
     1.4    val error: ('a -> 'b) -> 'a -> 'b
     1.5    val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
     1.6      'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
     1.7 -    (string -> 'd * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
     1.8 +    (bool * (string -> 'd * 'b list -> 'e list * ('d * 'b list))) option ->
     1.9 +    'd * 'a -> 'e list * ('d * 'c)
    1.10    val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    1.11      'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    1.12 -    (string -> 'b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
    1.13 +    (bool * (string -> 'b list -> 'd list * 'b list)) option -> 'a -> 'd list * 'c
    1.14    val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.15    val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.16    type lexicon
    1.17 @@ -252,21 +253,23 @@
    1.18  fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
    1.19    let
    1.20      val drain_with = drain def_prmpt get stopper;
    1.21 -
    1.22 -    fun drain_loop recover inp =
    1.23 -      drain_with (catch scanner) inp handle FAIL msg =>
    1.24 -        (drain_with (recover (the_default "Syntax error." msg)) inp);
    1.25 -
    1.26      val ((ys, (state', xs')), src') =
    1.27        (case (get def_prmpt src, opt_recover) of
    1.28          (([], s), _) => (([], (state, [])), s)
    1.29        | ((xs, s), NONE) => drain_with (error scanner) ((state, xs), s)
    1.30 -      | ((xs, s), SOME r) => drain_loop (unless (lift (one (#2 stopper))) o r) ((state, xs), s));
    1.31 +      | ((xs, s), SOME (interactive, recover)) =>
    1.32 +          let val inp = ((state, xs), s) in
    1.33 +            drain_with (catch scanner) inp handle FAIL msg =>
    1.34 +              let val err = the_default "Syntax error." msg in
    1.35 +                if interactive then Output.error_msg err else ();
    1.36 +                drain_with (unless (lift (one (#2 stopper))) (recover err)) inp
    1.37 +              end
    1.38 +          end);
    1.39    in (ys, (state', unget (xs', src'))) end;
    1.40  
    1.41  fun source def_prmpt get unget stopper scan opt_recover =
    1.42    unlift (source' def_prmpt get unget stopper (lift scan)
    1.43 -    (Option.map (fn r => lift o r) opt_recover));
    1.44 +    (Option.map (fn (int, r) => (int, lift o r)) opt_recover));
    1.45  
    1.46  fun single scan = scan >> (fn x => [x]);
    1.47  fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
     2.1 --- a/src/Pure/General/source.ML	Mon Jul 09 23:12:51 2007 +0200
     2.2 +++ b/src/Pure/General/source.ML	Tue Jul 10 00:17:52 2007 +0200
     2.3 @@ -22,10 +22,10 @@
     2.4    val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
     2.5    val tty: (string, unit) source
     2.6    val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     2.7 -    (string -> 'a * 'b list -> 'c list * ('a * 'b list)) option ->
     2.8 +    (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
     2.9      ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    2.10    val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
    2.11 -    (string -> 'a list -> 'b list * 'a list) option ->
    2.12 +    (bool * (string -> 'a list -> 'b list * 'a list)) option ->
    2.13      ('a, 'd) source -> ('b, ('a, 'd) source) source
    2.14  end;
    2.15  
     3.1 --- a/src/Pure/General/symbol.ML	Mon Jul 09 23:12:51 2007 +0200
     3.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 10 00:17:52 2007 +0200
     3.3 @@ -428,7 +428,8 @@
     3.4  in
     3.5  
     3.6  fun source do_recover src =
     3.7 -  Source.source stopper (Scan.bulk scan) (if do_recover then SOME (K recover) else NONE) src;
     3.8 +  Source.source stopper (Scan.bulk scan)
     3.9 +    (if do_recover then SOME (false, K recover) else NONE) src;
    3.10  
    3.11  end;
    3.12  
     4.1 --- a/src/Pure/Isar/outer_lex.ML	Mon Jul 09 23:12:51 2007 +0200
     4.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Jul 10 00:17:52 2007 +0200
     4.3 @@ -322,16 +322,14 @@
     4.4  
     4.5  val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
     4.6  
     4.7 -fun recover interactive msg x =
     4.8 -  (if interactive then Output.error_msg msg else ();
     4.9 -    (Scan.state :-- (fn pos => keep_line (Scan.many is_junk)
    4.10 -      >> (fn xs => [Token (pos, (Malformed msg, implode xs))])) >> #2) x);
    4.11 +fun recover msg = Scan.state :-- (fn pos =>
    4.12 +  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Malformed msg, implode xs))])) >> #2;
    4.13  
    4.14  in
    4.15  
    4.16  fun source do_recover get_lex pos src =
    4.17    Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
    4.18 -    (Option.map recover do_recover) src;
    4.19 +    (Option.map (rpair recover) do_recover) src;
    4.20  
    4.21  end;
    4.22  
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 09 23:12:51 2007 +0200
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 10 00:17:52 2007 +0200
     5.3 @@ -192,18 +192,17 @@
     5.4    let
     5.5      val no_terminator =
     5.6        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
     5.7 -    fun recover interactive msg x =
     5.8 -      (if interactive then Output.error_msg msg else ();
     5.9 -        (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x);
    5.10 +    fun recover int =
    5.11 +      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
    5.12    in
    5.13      src
    5.14      |> T.source_proper
    5.15      |> Source.source T.stopper
    5.16        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
    5.17 -      (Option.map recover do_recover)
    5.18 +        (Option.map recover do_recover)
    5.19      |> Source.map_filter I
    5.20      |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
    5.21 -      (Option.map recover do_recover)
    5.22 +        (Option.map recover do_recover)
    5.23      |> Source.map_filter I
    5.24    end;
    5.25