# HG changeset patch
# User wenzelm
# Date 1568492016 -7200
# Node ID 47ca5c7550e41341d98e0af24ebbee0e5271145d
# Parent  5d32cca55c2a2b52060f109b554f41f4a21a90e1
potentially more robust: read under lock if not yet set;

diff -r 5d32cca55c2a -r 47ca5c7550e4 src/Pure/Concurrent/single_assignment.ML
--- 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)) ())));