--- a/src/Pure/Concurrent/future.ML Thu Oct 22 15:19:44 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Oct 22 15:21:01 2009 +0200
@@ -153,9 +153,7 @@
Exn.capture (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) ()
else Exn.Exn Exn.Interrupt;
- val _ = Synchronized.change result
- (fn NONE => SOME res
- | SOME _ => raise Fail "Duplicate assignment of future value");
+ val _ = Synchronized.assign result (K (SOME res));
in
(case res of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
@@ -349,8 +347,7 @@
| SOME res => res);
fun join_wait x =
- Synchronized.guarded_access (result_of x)
- (fn NONE => NONE | some => SOME ((), some));
+ Synchronized.readonly_access (result_of x) (fn NONE => NONE | SOME _ => SOME ());
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE