src/Pure/General/source.ML

   val of_list: 'a list -> ('a, 'a list) source
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   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;
 
 structure Source: SOURCE =
 struct

     val ((ys, (state', xs')), src') =
       if null xs then (([], (state, [])), s)
       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 =
   make_source [] (init_state, src) (drain_source' stopper scan recover);
 
 
 (* non state-based *)
 
 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);
 
 end;