--- a/src/Pure/Concurrent/single_assignment.ML Fri Sep 13 11:00:59 2019 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Sat Sep 14 22:13:36 2019 +0200
@@ -28,32 +28,39 @@
fun var name = Var {name = name, state = Unsynchronized.ref (init_state ())};
-fun peek (Var {state, ...}) = (case ! state of Set x => SOME x | Unset _ => NONE);
+fun peek (Var {name, state}) =
+ (case ! state of
+ Set x => SOME x
+ | Unset {lock, ...} =>
+ Multithreading.synchronized name lock (fn () =>
+ (case ! state of
+ Set x => SOME x
+ | Unset _ => NONE)));
-fun await (v as Var {name, state}) =
+fun await (Var {name, state}) =
(case ! state of
Set x => x
| Unset {lock, cond} =>
Multithreading.synchronized name lock (fn () =>
let
fun wait () =
- (case peek v of
- NONE =>
+ (case ! state of
+ Unset _ =>
(case Multithreading.sync_wait NONE cond lock of
Exn.Res _ => wait ()
| Exn.Exn exn => Exn.reraise exn)
- | SOME x => x);
+ | Set x => x);
in wait () end));
fun assign_fail name = raise Fail ("Duplicate assignment to " ^ name);
-fun assign (v as Var {name, state}) x =
+fun assign (Var {name, state}) x =
(case ! state of
Set _ => assign_fail name
| Unset {lock, cond} =>
Multithreading.synchronized name lock (fn () =>
- (case peek v of
- SOME _ => assign_fail name
- | NONE =>
+ (case ! state of
+ Set _ => assign_fail name
+ | Unset _ =>
Thread_Attributes.uninterruptible (fn _ => fn () =>
(state := Set x; RunCall.clearMutableBit state; ConditionVar.broadcast cond)) ())));