# HG changeset patch
# User wenzelm
# Date 1184078703 -7200
# Node ID fb1102e98cd40bf6788f2bf62e83c31f74f570de
# Parent  5a4527f3ac796feb392fdc6c157fa9d15d3b9a2e
moved source cascading from scan.ML to source.ML;

diff -r 5a4527f3ac79 -r fb1102e98cd4 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Tue Jul 10 16:45:01 2007 +0200
+++ b/src/Pure/General/source.ML	Tue Jul 10 16:45:03 2007 +0200
@@ -136,24 +136,38 @@
 
 
 
-(** compose sources **)
-
-fun drain_source source stopper scan recover prompt src =
-  source prompt get_prompt unget stopper scan recover src;
-
+(** cascade sources **)
 
 (* state-based *)
 
+fun drain_source' stopper scan opt_recover prompt (state, src) =
+  let
+    val drain = Scan.drain prompt get_prompt stopper;
+    val (xs, s) = get_prompt prompt 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 (interactive, recover) =>
+            (drain (Scan.catch scan) inp handle Fail msg =>
+              (if interactive then Output.error_msg msg else ();
+                drain (Scan.unless (Scan.lift (Scan.one (#2 stopper))) (recover msg)) inp)));
+  in (ys, (state', unget (xs', src'))) end;
+
 fun source' init_state stopper scan recover src =
-  make_source [] (init_state, src) default_prompt
-    (drain_source Scan.source' stopper scan recover);
+  make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover);
 
 
 (* non state-based *)
 
+fun drain_source stopper scan opt_recover prompt =
+  Scan.unlift (drain_source' stopper (Scan.lift scan)
+    (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt);
+
 fun source stopper scan recover src =
-  make_source [] src default_prompt
-    (drain_source Scan.source stopper scan recover);
+  make_source [] src default_prompt (drain_source stopper scan recover);
 
 
 end;