--- a/src/Pure/goal.ML Wed Oct 17 14:58:04 2012 +0200
+++ b/src/Pure/goal.ML Wed Oct 17 21:04:51 2012 +0200
@@ -27,6 +27,7 @@
val fork_name: string -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val peek_futures: serial -> unit future list
+ val finish_futures: unit -> unit
val cancel_futures: unit -> unit
val future_enabled_level: int -> bool
val future_enabled: unit -> bool
@@ -173,6 +174,11 @@
fun peek_futures id =
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
+fun finish_futures () =
+ (case map_filter Task_Queue.group_status (#2 (Synchronized.value forked_proofs)) of
+ [] => ()
+ | exns => raise Par_Exn.make exns);
+
fun cancel_futures () =
Synchronized.change forked_proofs (fn (m, groups, tab) =>
(List.app Future.cancel_group groups; (0, [], Inttab.empty)));