--- 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 =