merged

--- a/src/Pure/Concurrent/future.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 22 15:22:41 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

--- a/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 15:22:41 2009 +0200
@@ -11,8 +11,10 @@
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
+  val readonly_access: 'a var -> ('a -> 'b option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
+  val assign: 'a var -> ('a -> 'a) -> unit
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -37,29 +39,48 @@
 
 (* synchronized access *)
 
-fun timed_access (Var {name, lock, cond, var}) time_limit f =
+fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f =
   SimpleThread.synchronized name lock (fn () =>
     let
       fun try_change () =
         let val x = ! var in
           (case f x of
-            SOME (y, x') => (var := x'; SOME y)
-          | NONE =>
+            NONE =>
               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
                 Exn.Result true => try_change ()
               | Exn.Result false => NONE
-              | Exn.Exn exn => reraise exn))
+              | Exn.Exn exn => reraise exn)
+          | SOME (y, x') =>
+              if readonly then SOME y
+              else
+                let
+                  val _ = magic_immutability_test var
+                    andalso raise Fail ("Attempt to change finished variable " ^ quote name);
+                  val _ = var := x';
+                  val _ = if finish then magic_immutability_mark var else ();
+                in SOME y end)
         end;
       val res = try_change ();
       val _ = ConditionVar.broadcast cond;
     in res end);
 
+fun timed_access var time_limit f =
+  access {time_limit = time_limit, readonly = false, finish = false} var f;
+
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
+fun readonly_access var f =
+  the (access {time_limit = K NONE, readonly = true, finish = false} var
+    (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))));
+
 
 (* unconditional change *)
 
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
+fun assign var f =
+  the (access {time_limit = K NONE, readonly = false, finish = true} var
+    (fn x => SOME ((), f x)));
+
 end;

--- a/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 22 15:22:41 2009 +0200
@@ -20,8 +20,13 @@
 
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
+fun readonly_access var f =
+  guarded_access var (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x)));
+
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
+val assign = change;
+
 end;
 end;

--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 22 15:22:41 2009 +0200
@@ -128,3 +128,12 @@
         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
       in Exn.release res end;
 
+
+(* magic immutability -- for internal use only! *)
+
+fun magic_immutability_mark (r: 'a Unsynchronized.ref) =
+  ignore (RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r);
+
+fun magic_immutability_test (r: 'a Unsynchronized.ref) =
+  Word8.andb (0wx40, RunCall.run_call1 RuntimeCalls.POLY_SYS_get_flags r) = 0w0;
+

--- a/src/Pure/ML-Systems/smlnj.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Oct 22 15:22:41 2009 +0200
@@ -66,6 +66,10 @@
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
 
 (*dummy implementation*)
+fun magic_immutability_test _ = false;
+fun magic_immutability_mark _ = ();
+
+(*dummy implementation*)
 fun profile (n: int) f x = f x;
 
 (*dummy implementation*)
@@ -177,8 +181,6 @@
 
 val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
 
-
-(*Convert a process ID to a decimal string (chiefly for tracing)*)
 fun process_id pid =
   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));