# HG changeset patch
# User wenzelm
# Date 1414866831 -3600
# Node ID 505a8150368a86a5b586aca02255f778378aca58
# Parent  64e571275b36751e827a71a0091ed741381fac8a
recover via scanner;
tuned signature;

diff -r 64e571275b36 -r 505a8150368a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/General/scan.ML
--- 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 *)
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/General/source.ML
--- 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;
diff -r 64e571275b36 -r 505a8150368a src/Pure/General/symbol.ML
--- 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;
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/General/symbol_pos.ML
--- 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 *)
diff -r 64e571275b36 -r 505a8150368a src/Pure/Isar/outer_syntax.ML
--- 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;
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/Isar/token.ML
--- 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) =
diff -r 64e571275b36 -r 505a8150368a src/Pure/ML/ml_lex.ML
--- 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;
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/ML/ml_parse.ML
--- 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);
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/Thy/thy_header.ML
--- 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
diff -r 64e571275b36 -r 505a8150368a src/Pure/Thy/thy_output.ML
--- 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;
 
 
diff -r 64e571275b36 -r 505a8150368a src/Pure/Thy/thy_syntax.ML
--- 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;