# HG changeset patch
# User wenzelm
# Date 978115453 -3600
# Node ID 01e2d857fb7837f1ee9d1c16ec63675f9361cbf9
# Parent  0f3537fad0f329a3ca253964aa15155650fee575
recover: result;

diff -r 0f3537fad0f3 -r 01e2d857fb78 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Fri Dec 29 19:43:52 2000 +0100
+++ b/src/Pure/General/scan.ML	Fri Dec 29 19:44:13 2000 +0100
@@ -55,10 +55,10 @@
   val error: ('a -> 'b) -> 'a -> 'b
   val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
     'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
-    ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
+    ('d * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
   val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
     'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
-    ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
+    ('b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
   val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   type lexicon
@@ -207,12 +207,11 @@
 
 fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
   let
-    fun drain_with scan = drain def_prmpt get stopper scan;
+    val drain_with = drain def_prmpt get stopper;
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (error_msg (if_none msg "Syntax error.");
-          drain_loop recover (apfst snd (drain_with recover inp)));
+        (error_msg (if_none msg "Syntax error."); drain_with recover inp);
 
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
diff -r 0f3537fad0f3 -r 01e2d857fb78 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Fri Dec 29 19:43:52 2000 +0100
+++ b/src/Pure/General/source.ML	Fri Dec 29 19:44:13 2000 +0100
@@ -23,10 +23,10 @@
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
-    ('a * 'b list -> 'd * ('a * 'b list)) option ->
+    ('a * 'b list -> 'c list * ('a * 'b list)) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
-    ('a list -> 'c * 'a list) option ->
+    ('a list -> 'b list * 'a list) option ->
     ('a, 'd) source -> ('b, ('a, 'd) source) source
 end;