merged

--- a/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 15:52:33 2012 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 20:45:15 2012 +0200
@@ -28,7 +28,7 @@
       with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
     qed
   qed
-  with `\<not> (\<forall>x. P x)` show ?thesis ..
+  with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
 qed
 
 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"

--- a/src/HOL/ROOT	Thu Oct 18 15:52:33 2012 +0200
+++ b/src/HOL/ROOT	Thu Oct 18 20:45:15 2012 +0200
@@ -623,7 +623,7 @@
 
 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   description {* Examples for Bounded Natural Functors *}
-  options [document = false, threads = 1]
+  options [document = false]
   theories
     Lambda_Term
     Process

--- a/src/Pure/PIDE/protocol.ML	Thu Oct 18 15:52:33 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Oct 18 20:45:15 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 15:52:33 2012 +0200
+++ b/src/Pure/System/session.ML	Thu Oct 18 20:45:15 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 15:52:33 2012 +0200
+++ b/src/Pure/goal.ML	Thu Oct 18 20:45:15 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;