# HG changeset patch
# User wenzelm
# Date 961969599 -7200
# Node ID addbea3446738dc2bd47646a65dfb8805b56cc5e
# Parent  25245986e6670dada1100222bcbd12613f0ac51c
added state: 'a * 'b -> 'a * ('a * 'b);

diff -r 25245986e667 -r addbea344673 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sun Jun 25 23:46:22 2000 +0200
+++ b/src/Pure/General/scan.ML	Sun Jun 25 23:46:39 2000 +0200
@@ -40,6 +40,7 @@
   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
   val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
   val first: ('a -> 'b) list -> 'a -> 'b
+  val state: 'a * 'b -> 'a * ('a * 'b) 
   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
@@ -145,6 +146,8 @@
 
 (* state based scanners *)
 
+fun state (st, xs) = (st, (st, xs));
+
 fun depend scan (st, xs) =
   let val ((st', y), xs') = scan st xs
   in (y, (st', xs')) end;