--- a/src/Pure/System/session.ML Mon Feb 25 13:31:02 2013 +0100
+++ b/src/Pure/System/session.ML Mon Feb 25 17:47:32 2013 +0100
@@ -67,14 +67,8 @@
(* finish *)
-fun finish_futures () =
- (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
- [] => ()
- | exns => raise Par_Exn.make exns);
-
fun finish () =
- (Future.shutdown ();
- finish_futures ();
+ (Goal.shutdown_futures ();
Thy_Info.finish ();
Present.finish ();
Keyword.status ();
--- a/src/Pure/goal.ML Mon Feb 25 13:31:02 2013 +0100
+++ b/src/Pure/goal.ML Mon Feb 25 17:47:32 2013 +0100
@@ -28,6 +28,7 @@
val fork: int -> (unit -> 'a) -> 'a future
val peek_futures: serial -> unit future list
val reset_futures: unit -> Future.group list
+ val shutdown_futures: unit -> unit
val future_enabled_level: int -> bool
val future_enabled: unit -> bool
val future_enabled_nested: int -> bool
@@ -178,6 +179,12 @@
Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
+fun shutdown_futures () =
+ (Future.shutdown ();
+ (case map_filter Task_Queue.group_status (reset_futures ()) of
+ [] => ()
+ | exns => raise Par_Exn.make exns));
+
end;