# HG changeset patch
# User wenzelm
# Date 954612955 -7200
# Node ID a88e91792f0ac6b4b6ca69c1fea745e6f41925d8
# Parent  39a695b0b1d7e3e49d3cf6b0d599fd1164b187aa
recover: observe stopper;

diff -r 39a695b0b1d7 -r a88e91792f0a src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat Apr 01 20:13:33 2000 +0200
+++ b/src/Pure/General/scan.ML	Sat Apr 01 20:15:55 2000 +0200
@@ -214,10 +214,8 @@
       (case (get def_prmpt src, opt_recover) of
         (([], s), _) => (([], (state, [])), s)
       | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
-      | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
-  in
-    (ys, (state', unget (xs', src')))
-  end;
+      | ((xs, s), Some r) => drain_loop (unless (lift (one (#2 stopper))) r) ((state, xs), s));
+  in (ys, (state', unget (xs', src'))) end;
 
 fun source def_prmpt get unget stopper scan opt_recover src =
   let val (ys, ((), src')) =