more basic Goal.reset_futures as snapshot of implicit state;
more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

--- a/src/Pure/PIDE/protocol.ML	Thu Oct 18 19:12:58 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Oct 18 19:58:30 2012 +0200
@@ -59,7 +59,7 @@
               in pair int (list (pair int (option int))) end
               |> YXML.string_of_body);
 
-        val _ = Goal.cancel_futures ();
+        val _ = List.app Future.cancel_group (Goal.reset_futures ());
         val _ = Isabelle_Process.reset_tracing_limits ();
         val _ = Document.start_execution state';
       in state' end));

--- a/src/Pure/System/session.ML	Thu Oct 18 19:12:58 2012 +0200
+++ b/src/Pure/System/session.ML	Thu Oct 18 19:58:30 2012 +0200
@@ -66,15 +66,18 @@
 
 (* 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 ();
-  Goal.finish_futures ();
+  finish_futures ();
   Thy_Info.finish ();
   Present.finish ();
   Keyword.status ();
   Outer_Syntax.check_syntax ();
-  Goal.cancel_futures ();
-  Future.shutdown ();
   Options.reset_default ();
   session_finished := true);
 

--- a/src/Pure/goal.ML	Thu Oct 18 19:12:58 2012 +0200
+++ b/src/Pure/goal.ML	Thu Oct 18 19:58:30 2012 +0200
@@ -27,8 +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 reset_futures: unit -> Future.group list
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool
@@ -174,14 +173,9 @@
 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)));
+fun reset_futures () =
+  Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
+    (groups, (0, [], Inttab.empty)));
 
 end;