more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;

--- a/src/Pure/System/session.ML	Wed Oct 17 14:58:04 2012 +0200
+++ b/src/Pure/System/session.ML	Wed Oct 17 21:04:51 2012 +0200
@@ -72,6 +72,8 @@
     Keyword.status ();
     Outer_Syntax.check_syntax ();
     Future.shutdown ();
+    Goal.finish_futures ();
+    Goal.cancel_futures ();
     Options.reset_default ();
     session_finished := true);
 

--- 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)));