# 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