simplified -- scanning is never interactive;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -131,7 +131,7 @@
   in
     Source.of_string name
     |> Symbol.source
-    |> Token.source {do_recover = SOME false} lex Position.start
+    |> Token.source {do_recover = true} lex Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse.xthms1 >> get) NONE
     |> Source.exhaust

--- a/src/Pure/General/source.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/General/source.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -18,10 +18,10 @@
   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)) ->
-    (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
+    (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) ->
-    (bool * (string -> 'a list -> 'b list * 'a list)) option ->
+    (string -> 'a list -> 'b list * 'a list) option ->
     ('a, 'd) source -> ('b, ('a, 'd) source) source
 end;
 
@@ -117,11 +117,10 @@
       else
         (case opt_recover of
           NONE => drain (Scan.error scan) inp
-        | SOME (interactive, recover) =>
+        | SOME recover =>
             (drain (Scan.catch scan) inp handle Fail msg =>
-              (if interactive then Output.error_message msg else ();
-                drain (Scan.unless (Scan.lift (Scan.one (Scan.is_stopper stopper))) (recover msg))
-                  inp)));
+              (drain (Scan.unless (Scan.lift (Scan.one (Scan.is_stopper stopper))) (recover msg))
+                inp)));
   in (ys, (state', unget (xs', src'))) end;
 
 fun source' init_state stopper scan recover src =
@@ -132,7 +131,7 @@
 
 fun drain_source stopper scan opt_recover =
   Scan.unlift (drain_source' stopper (Scan.lift scan)
-    (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover));
+    (Option.map (fn r => Scan.lift o r) opt_recover));
 
 fun source stopper scan recover src =
   make_source [] src (drain_source stopper scan recover);

--- a/src/Pure/Isar/outer_syntax.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -236,13 +236,13 @@
 fun scan lexs pos =
   Source.of_string #>
   Symbol.source #>
-  Token.source {do_recover = SOME false} (K lexs) pos #>
+  Token.source {do_recover = true} (K lexs) pos #>
   Source.exhaust;
 
 fun parse (lexs, syntax) pos str =
   Source.of_string str
   |> Symbol.source
-  |> Token.source {do_recover = SOME false} (K lexs) pos
+  |> Token.source {do_recover = true} (K lexs) pos
   |> commands_source syntax
   |> Source.exhaust;
 

--- a/src/Pure/Isar/token.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -79,9 +79,9 @@
   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 option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  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 option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source: {do_recover: bool} -> (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
@@ -562,7 +562,7 @@
 
 fun source' {do_recover} get_lex =
   Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
-    (Option.map (rpair recover) do_recover);
+    (if do_recover then SOME recover else NONE);
 
 fun source do_recover get_lex pos src =
   Symbol_Pos.source pos src
@@ -582,7 +582,7 @@
 
 fun read lex scan (syms, pos) =
   Source.of_list syms
-  |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+  |> source' {do_recover = false} (K (lex, Scan.empty_lexicon))
   |> source_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
   |> Source.exhaust;

--- a/src/Pure/ML/ml_lex.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -308,7 +308,7 @@
     val input =
       Source.of_list syms
       |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan))
-        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+        (SOME (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 +318,7 @@
 
 fun source src =
   Symbol_Pos.source (Position.line 1) src
-  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
+  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME recover);
 
 val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 

--- a/src/Pure/Thy/thy_header.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -127,7 +127,7 @@
   str
   |> Source.of_string_limited 8000
   |> Symbol.source
-  |> Token.source {do_recover = NONE} (K header_lexicons) pos;
+  |> Token.source {do_recover = false} (K header_lexicons) pos;
 
 fun read_source pos source =
   let val res =