src/Pure/Concurrent/lazy.ML
changeset 68597 afa7c5a239e6
parent 68590 f3c3c1e6133a
child 68697 d81a5da01796
--- a/src/Pure/Concurrent/lazy.ML	Fri Jul 06 10:44:45 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Fri Jul 06 15:35:48 2018 +0200
@@ -89,7 +89,11 @@
                   (fn Expr (name, e) =>
                         let val x = Future.promise_name name I
                         in ((SOME (name, e), x), Result x) end
-                    | Result x => ((NONE, x), Result x));
+                    | Result x => ((NONE, x), Result x))
+                  handle exn as Fail _ =>
+                    (case Synchronized.value var of
+                      Expr _ => Exn.reraise exn
+                    | Result x => (NONE, x));
             in
               (case expr of
                 SOME (name, e) =>
@@ -102,7 +106,7 @@
                     val _ =
                       if Exn.is_interrupt_exn res
                       then Synchronized.change var (fn _ => Expr (name, e))
-                      else Synchronized.change var (fn _ => Result (Future.value_result res));
+                      else Synchronized.assign var (Result (Future.value_result res));
                   in res end
               | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
             end) ());