--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Nov 01 19:33:51 2014 +0100
@@ -131,9 +131,9 @@
in
Source.of_string name
|> Symbol.source
- |> Token.source {do_recover = true} lex Position.start
+ |> Token.source lex Position.start
|> Token.source_proper
- |> Source.source Token.stopper (Parse.xthms1 >> get) NONE
+ |> Source.source Token.stopper (Parse.xthms1 >> get)
|> Source.exhaust
end
--- a/src/Pure/General/scan.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/General/scan.ML Sat Nov 01 19:33:51 2014 +0100
@@ -41,6 +41,7 @@
val permissive: ('a -> 'b) -> 'a -> 'b
val error: ('a -> 'b) -> 'a -> 'b
val catch: ('a -> 'b) -> 'a -> 'b (*exception Fail*)
+ val recover: ('a -> 'b) -> (string -> 'a -> 'b) -> 'a -> 'b
val fail: 'a -> 'b
val fail_with: ('a -> message) -> 'a -> 'b
val succeed: 'a -> 'b -> 'a * 'b
@@ -110,6 +111,9 @@
handle ABORT msg => raise Fail (msg ())
| FAIL msg => raise Fail (case msg of NONE => "Syntax error" | SOME m => m ());
+fun recover scan1 scan2 xs =
+ catch scan1 xs handle Fail msg => scan2 msg xs;
+
(* scanner combinators *)
--- a/src/Pure/General/source.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/General/source.ML Sat Nov 01 19:33:51 2014 +0100
@@ -18,10 +18,8 @@
val of_string: string -> (string, string list) source
val of_string_limited: int -> string -> (string, substring) source
val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
- (string -> 'a * 'b list -> 'c list * ('a * 'b list)) option ->
('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
- (string -> 'a list -> 'b list * 'a list) option ->
('a, 'd) source -> ('b, ('a, 'd) source) source
end;
@@ -107,33 +105,25 @@
(* state-based *)
-fun drain_source' stopper scan opt_recover (state, src) =
+fun drain_source' stopper scan (state, src) =
let
val drain = Scan.drain get stopper;
val (xs, s) = get src;
- val inp = ((state, xs), s);
val ((ys, (state', xs')), src') =
if null xs then (([], (state, [])), s)
- else
- (case opt_recover of
- NONE => drain (Scan.error scan) inp
- | SOME recover =>
- (drain (Scan.catch scan) inp handle Fail msg =>
- (drain (Scan.unless (Scan.lift (Scan.one (Scan.is_stopper stopper))) (recover msg))
- inp)));
+ else drain (Scan.error scan) ((state, xs), s);
in (ys, (state', unget (xs', src'))) end;
-fun source' init_state stopper scan recover src =
- make_source [] (init_state, src) (drain_source' stopper scan recover);
+fun source' init_state stopper scan src =
+ make_source [] (init_state, src) (drain_source' stopper scan);
(* non state-based *)
-fun drain_source stopper scan opt_recover =
- Scan.unlift (drain_source' stopper (Scan.lift scan)
- (Option.map (fn r => Scan.lift o r) opt_recover));
+fun drain_source stopper scan =
+ Scan.unlift (drain_source' stopper (Scan.lift scan));
-fun source stopper scan recover src =
- make_source [] src (drain_source stopper scan recover);
+fun source stopper scan src =
+ make_source [] src (drain_source stopper scan);
end;
--- a/src/Pure/General/symbol.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/General/symbol.ML Sat Nov 01 19:33:51 2014 +0100
@@ -438,7 +438,7 @@
in
-fun source src = Source.source stopper (Scan.bulk scan_total) NONE src;
+fun source src = Source.source stopper (Scan.bulk scan_total) src;
end;
--- a/src/Pure/General/symbol_pos.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Nov 01 19:33:51 2014 +0100
@@ -224,7 +224,7 @@
fun source pos =
Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
- Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos)))))) NONE;
+ Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos))))));
(* compact representation -- with Symbol.DEL padding *)
--- a/src/Pure/Isar/outer_syntax.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sat Nov 01 19:33:51 2014 +0100
@@ -224,9 +224,9 @@
fun commands_source syntax =
Token.source_proper #>
- Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) NONE #>
+ Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
Source.map_filter I #>
- Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command syntax) xs)) NONE;
+ Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command syntax) xs));
end;
@@ -236,13 +236,13 @@
fun scan lexs pos =
Source.of_string #>
Symbol.source #>
- Token.source {do_recover = true} (K lexs) pos #>
+ Token.source (K lexs) pos #>
Source.exhaust;
fun parse (lexs, syntax) pos str =
Source.of_string str
|> Symbol.source
- |> Token.source {do_recover = true} (K lexs) pos
+ |> Token.source (K lexs) pos
|> commands_source syntax
|> Source.exhaust;
--- a/src/Pure/Isar/token.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/Isar/token.ML Sat Nov 01 19:33:51 2014 +0100
@@ -79,9 +79,10 @@
val pretty_src: Proof.context -> src -> Pretty.T
val ident_or_symbolic: string -> bool
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
- val source': {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
- val source: {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ val source: (unit -> Scan.lexicon * Scan.lexicon) ->
+ Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
+ (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ val source_strict: (unit -> Scan.lexicon * Scan.lexicon) ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
type 'a parser = T list -> 'a * T list
@@ -560,13 +561,14 @@
in
-fun source' {do_recover} get_lex =
- Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
- (if do_recover then SOME recover else NONE);
+fun source' strict get_lex =
+ let
+ val scan_strict = Scan.bulk (fn xs => scan (get_lex ()) xs);
+ val scan = if strict then scan_strict else Scan.recover scan_strict recover;
+ in Source.source Symbol_Pos.stopper scan end;
-fun source do_recover get_lex pos src =
- Symbol_Pos.source pos src
- |> source' do_recover get_lex;
+fun source get_lex pos src = Symbol_Pos.source pos src |> source' false get_lex;
+fun source_strict get_lex pos src = Symbol_Pos.source pos src |> source' true get_lex;
end;
@@ -582,9 +584,9 @@
fun read lex scan (syms, pos) =
Source.of_list syms
- |> source' {do_recover = false} (K (lex, Scan.empty_lexicon))
+ |> source' true (K (lex, Scan.empty_lexicon))
|> source_proper
- |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+ |> Source.source stopper (Scan.error (Scan.bulk scan))
|> Source.exhaust;
fun read_antiq lex scan (syms, pos) =
--- a/src/Pure/ML/ml_lex.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Sat Nov 01 19:33:51 2014 +0100
@@ -307,8 +307,9 @@
| check _ = ();
val input =
Source.of_list syms
- |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan))
- (SOME (fn msg => recover msg >> map Antiquote.Text))
+ |> Source.source Symbol_Pos.stopper
+ (Scan.recover (Scan.bulk (!!! "bad input" scan))
+ (fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
|> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
|> tap (List.app check);
@@ -318,7 +319,7 @@
fun source src =
Symbol_Pos.source (Position.line 1) src
- |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME recover);
+ |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover);
val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
--- a/src/Pure/ML/ml_parse.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/ML/ml_parse.ML Sat Nov 01 19:33:51 2014 +0100
@@ -57,7 +57,7 @@
ML_System.is_smlnj ?
(Source.of_string #>
ML_Lex.source #>
- Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE #>
+ Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) #>
Source.exhaust #>
implode);
--- a/src/Pure/Thy/thy_header.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Sat Nov 01 19:33:51 2014 +0100
@@ -127,13 +127,13 @@
str
|> Source.of_string_limited 8000
|> Symbol.source
- |> Token.source {do_recover = false} (K header_lexicons) pos;
+ |> Token.source_strict (K header_lexicons) pos;
fun read_source pos source =
let val res =
source
|> Token.source_proper
- |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
+ |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
|> Source.get_single;
in
(case res of
--- a/src/Pure/Thy/thy_output.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Nov 01 19:33:51 2014 +0100
@@ -415,8 +415,8 @@
val spans = toks
|> take_suffix Token.is_space |> #1
|> Source.of_list
- |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
- |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
+ |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token))
+ |> Source.source stopper (Scan.error (Scan.bulk span))
|> Source.exhaust;
--- a/src/Pure/Thy/thy_syntax.ML Sat Nov 01 18:46:48 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sat Nov 01 19:33:51 2014 +0100
@@ -105,7 +105,7 @@
val parse_elements =
Source.of_list #>
- Source.source stopper (Scan.bulk other_element) NONE #>
+ Source.source stopper (Scan.bulk other_element) #>
Source.exhaust;
end;