src/Pure/Concurrent/lazy.ML

--- a/src/Pure/Concurrent/lazy.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -10,6 +10,8 @@
 sig
   type 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
+  val is_finished: 'a lazy -> bool
+  val get_finished: 'a lazy -> 'a
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
@@ -36,6 +38,13 @@
 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
+fun is_finished x = is_some (peek x);
+
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished lazy evaluation");
+
 
 (* force result *)