1.1 --- a/src/Pure/thm.ML Wed Oct 01 08:42:42 2008 +0200
1.2 +++ b/src/Pure/thm.ML Wed Oct 01 12:00:00 2008 +0200
1.3 @@ -1612,8 +1612,17 @@
1.4 fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
1.5
1.6 fun join_futures thy =
1.7 - (case CRITICAL (fn () => ! (Futures.get thy)) of [] => ()
1.8 - | futures => (Future.release_results (Future.join_results (rev futures)); join_futures thy));
1.9 + let
1.10 + val futures = Futures.get thy;
1.11 + fun joined () =
1.12 + (Future.join_results (rev (! futures));
1.13 + CRITICAL (fn () =>
1.14 + let
1.15 + val (finished, unfinished) = List.partition Future.is_finished (! futures);
1.16 + val _ = futures := unfinished;
1.17 + in finished end)
1.18 + |> Future.join_results |> Exn.release_all |> null);
1.19 + in while not (joined ()) do () end;
1.20
1.21
1.22 (* promise *)
1.23 @@ -1658,7 +1667,7 @@
1.24
1.25 fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
1.26 let
1.27 - val _ = Future.release_results (Future.join_results (rev (map #2 promises)));
1.28 + val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
1.29 val results = map (apsnd Future.join) promises;
1.30 val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
1.31 results Inttab.empty;