src/Pure/Concurrent/synchronized.ML

--- a/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 09:50:29 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 15:19:44 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;