# HG changeset patch
# User wenzelm
# Date 1596624163 -7200
# Node ID 3afd6b1c7ab5aba8f744ebef52c7bf5376faba54
# Parent  df99d26efeebeb84b8bdb615e111a91fe66dedde
more robust: insist in finished future;

diff -r df99d26efeeb -r 3afd6b1c7ab5 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Aug 05 12:34:23 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 05 12:42:43 2020 +0200
@@ -27,6 +27,7 @@
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
   val fork: (unit -> 'a) -> 'a future
+  val get_result: 'a future -> 'a Exn.result
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
diff -r df99d26efeeb -r 3afd6b1c7ab5 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Aug 05 12:34:23 2020 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed Aug 05 12:42:43 2020 +0200
@@ -103,7 +103,7 @@
                   let
                     val res0 = Exn.capture (restore_attributes e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                    val res = Future.join_result x;
+                    val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))