# HG changeset patch # User wenzelm # Date 1256217661 -7200 # Node ID e3e61133e0fc7fe8adf8a609a8cff9d7bc530fd7 # Parent e66b41782cb59e9e12028c7f0e8baa856eb67992 use Synchronized.assign to achieve actual immutable results; diff -r e66b41782cb5 -r e3e61133e0fc src/Pure/Concurrent/future.ML --- 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