# HG changeset patch
# User wenzelm
# Date 1231547283 -3600
# Node ID fdf396a24a9f31f8696749e242222ea8545f5b9d
# Parent  db532e37cda2b5fd7849bf181da4c729f42a5fe4
added force_result;

diff -r db532e37cda2 -r fdf396a24a9f src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Sat Jan 10 00:25:31 2009 +0100
+++ b/src/Pure/General/lazy.ML	Sat Jan 10 01:28:03 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/lazy.ML
-    ID:         $Id$
     Author:     Florian Haftmann and Makarius, TU Muenchen
 
 Lazy evaluation with memoing.  Concurrency may lead to multiple
@@ -13,6 +12,7 @@
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
+  val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
 end
@@ -41,7 +41,7 @@
 
 (* force result *)
 
-fun force r =
+fun force_result r =
   let
     (*potentially concurrent evaluation*)
     val res =
@@ -53,7 +53,9 @@
       (case ! r of
         Lazy _ => (r := Result res; res)
       | Result res' => res'));
-  in Exn.release res' end;
+  in res' end;
+
+fun force r = Exn.release (force_result r);
 
 fun map_force f = value o f o force;