# HG changeset patch
# User wenzelm
# Date 1201215075 -3600
# Node ID 94a515ed8a39d21ec198ce2f72228bd078811a3f
# Parent  682e84b60e5c8f8c747fc13f63c9847814bf4d0b
added combinator for wrapped lazy evaluation;

diff -r 682e84b60e5c -r 94a515ed8a39 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Thu Jan 24 23:51:13 2008 +0100
+++ b/src/Pure/General/seq.ML	Thu Jan 24 23:51:15 2008 +0100
@@ -33,6 +33,7 @@
   val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
   val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
   val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
+  val wrap: ((unit -> ('a * 'a seq) option) -> ('a * 'a seq) option) -> 'a seq -> 'a seq
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
   val succeed: 'a -> 'a seq
@@ -163,6 +164,12 @@
 
 fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
 
+(*wrapped lazy evaluation*)
+fun wrap f xq =
+  make (fn () =>
+    (case f (fn () => pull xq) of
+      NONE => NONE
+    | SOME (x, xq') => SOME (x, wrap f xq')));
 
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =