# HG changeset patch
# User wenzelm
# Date 1350583110 -7200
# Node ID 85780e6f8fd264cf6c78edd6cfe0cab9ef3808e0
# Parent  defce6616890af80ad44cdab458a68dc711b7e7c
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);

diff -r defce6616890 -r 85780e6f8fd2 src/Pure/PIDE/protocol.ML
--- 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));
diff -r defce6616890 -r 85780e6f8fd2 src/Pure/System/session.ML
--- 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);
 
diff -r defce6616890 -r 85780e6f8fd2 src/Pure/goal.ML
--- 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;