store immutable result: fewer refs, mutexes, condvars;
authorwenzelm
Thu, 05 Jul 2018 23:08:01 +0200
changeset 68590 f3c3c1e6133a
parent 68589 9258f16d68b4
child 68591 90381a0f5474
store immutable result: fewer refs, mutexes, condvars;
src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Jul 04 22:44:24 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jul 05 23:08:01 2018 +0200
@@ -100,9 +100,9 @@
                     (*semantic race: some other threads might see the same
                       interrupt, until there is a fresh start*)
                     val _ =
-                      if Exn.is_interrupt_exn res then
-                        Synchronized.change var (fn _ => Expr (name, e))
-                      else ();
+                      if Exn.is_interrupt_exn res
+                      then Synchronized.change var (fn _ => Expr (name, e))
+                      else Synchronized.change var (fn _ => Result (Future.value_result res));
                   in res end
               | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
             end) ());