# HG changeset patch
# User wenzelm
# Date 1346359092 -7200
# Node ID 8e124393c281488312e617bb9da820a59aac6b30
# Parent  b77e1910af8ac60304a5e5331c95a00cdb3015e1# Parent  1266b51f9bbc77e51dd7b65bae5e661b28359c62
merged;

diff -r b77e1910af8a -r 8e124393c281 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -73,7 +73,6 @@
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val shutdown: unit -> unit
-  val status: (unit -> 'a) -> 'a
   val group_tasks: group -> task list
   val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
 end;
@@ -642,20 +641,6 @@
   else ();
 
 
-(* status markup *)
-
-fun status e =
-  let
-    val task_props =
-      (case worker_task () of
-        NONE => I
-      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
-    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
-    val x = e ();  (*sic -- report "joined" only for success*)
-    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
-  in x end;
-
-
 (* queue status *)
 
 fun group_tasks group = Task_Queue.group_tasks (! queue) group;
diff -r b77e1910af8a -r 8e124393c281 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/General/stack.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -10,7 +10,9 @@
   val level: 'a T -> int
   val init: 'a -> 'a T
   val top: 'a T -> 'a
+  val bottom: 'a T -> 'a
   val map_top: ('a -> 'a) -> 'a T -> 'a T
+  val map_bottom: ('a -> 'a) -> 'a T -> 'a T
   val map_all: ('a -> 'a) -> 'a T -> 'a T
   val push: 'a T -> 'a T
   val pop: 'a T -> 'a T      (*exception List.Empty*)
@@ -27,8 +29,16 @@
 
 fun top (x, _) = x;
 
+fun bottom (x, []) = x
+  | bottom (_, xs) = List.last xs;
+
 fun map_top f (x, xs) = (f x, xs);
 
+fun map_bottom f (x, []) = (f x, [])
+  | map_bottom f (x, rest) =
+      let val (ys, z) = split_last rest
+      in (x, ys @ [f z]) end;
+
 fun map_all f (x, xs) = (f x, map f xs);
 
 fun push (x, xs) = (x, x :: xs);
diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -265,7 +265,7 @@
 (* global endings *)
 
 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
-val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
+val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -21,6 +21,9 @@
   val propagate_ml_env: state -> state
   val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
+  val begin_proofs: state -> state
+  val register_proofs: thm list -> state -> state
+  val join_recent_proofs: state -> unit
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val set_facts: thm list -> state -> state
@@ -168,8 +171,11 @@
 fun init ctxt =
   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
 
-fun current (State st) = Stack.top st |> (fn Node node => node);
-fun map_current f (State st) = State (Stack.map_top (map_node f) st);
+fun top (State st) = Stack.top st |> (fn Node node => node);
+fun bottom (State st) = Stack.bottom st |> (fn Node node => node);
+
+fun map_top f (State st) = State (Stack.map_top (map_node f) st);
+fun map_bottom f (State st) = State (Stack.map_bottom (map_node f) st);
 fun map_all f (State st) = State (Stack.map_all (map_node f) st);
 
 
@@ -195,18 +201,21 @@
 
 (* context *)
 
-val context_of = #context o current;
+val context_of = #context o top;
 val theory_of = Proof_Context.theory_of o context_of;
 
 fun map_node_context f =
   map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context f =
-  map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+  map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context_result f state =
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
+fun map_context_bottom f =
+  map_bottom (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun propagate_ml_env state = map_contexts
@@ -216,9 +225,17 @@
 val put_thms = map_context oo Proof_Context.put_thms;
 
 
+(* forked proofs *)
+
+val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
+val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
+
+val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
+
+
 (* facts *)
 
-val get_facts = #facts o current;
+val get_facts = #facts o top;
 
 fun the_facts state =
   (case get_facts state of SOME facts => facts
@@ -229,7 +246,7 @@
   | _ => error "Single theorem expected");
 
 fun put_facts facts =
-  map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
+  map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   put_thms true (Auto_Bind.thisN, facts);
 
 val set_facts = put_facts o SOME;
@@ -249,8 +266,8 @@
 
 (* mode *)
 
-val get_mode = #mode o current;
-fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
+val get_mode = #mode o top;
+fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
 
 val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
 
@@ -274,7 +291,7 @@
 (* current goal *)
 
 fun current_goal state =
-  (case current state of
+  (case top state of
     {context, goal = SOME (Goal goal), ...} => (context, goal)
   | _ => error "No current goal");
 
@@ -285,7 +302,7 @@
     else state
   end;
 
-fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
 
 val set_goal = put_goal o SOME;
 val reset_goal = put_goal NONE;
@@ -338,7 +355,7 @@
 
 fun pretty_state nr state =
   let
-    val {context = ctxt, facts, mode, goal = _} = current state;
+    val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
     fun levels_up 0 = ""
@@ -922,6 +939,7 @@
       |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
   in
     outer_state
+    |> register_proofs (flat results)
     |> map_context (after_ctxt props)
     |> pair (after_qed, results)
   end;
@@ -1120,19 +1138,21 @@
 
 local
 
-fun future_terminal_proof proof1 proof2 meths int state =
-  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
-  then proof1 meths state
-  else snd (proof2 (fn state' =>
-    Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state);
+fun future_terminal_proof n proof1 proof2 meths int state =
+  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
+    andalso not (is_relevant state)
+  then
+    snd (proof2 (fn state' =>
+      Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
+  else proof1 meths state;
 
 in
 
 fun local_future_terminal_proof x =
-  future_terminal_proof local_terminal_proof local_future_proof x;
+  future_terminal_proof 2 local_terminal_proof local_future_proof x;
 
 fun global_future_terminal_proof x =
-  future_terminal_proof global_terminal_proof global_future_proof x;
+  future_terminal_proof 3 global_terminal_proof global_future_proof x;
 
 end;
 
diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -53,9 +53,10 @@
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val is_malformed: transition -> bool
-  val theory: (theory -> theory) -> transition -> transition
+  val join_recent_proofs: state -> unit
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
+  val theory: (theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
   val open_target: (generic_theory -> local_theory) -> transition -> transition
@@ -422,15 +423,21 @@
 val unknown_context = imperative (fn () => warning "Unknown context");
 
 
-(* theory transitions *)
+(* forked proofs *)
+
+val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
+val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
 
-val global_theory_group =
-  Sign.new_group #>
-  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+fun join_recent_proofs st =
+  (case try proof_of st of
+    SOME prf => Proof.join_recent_proofs prf
+  | NONE =>
+      (case try theory_of st of
+        SOME thy => Thm.join_recent_proofs thy
+      | NONE => ()));
 
-val local_theory_group =
-  Local_Theory.new_group #>
-  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
+(* theory transitions *)
 
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
@@ -439,7 +446,8 @@
 fun theory' f = transaction (fn int =>
   (fn Theory (Context.Theory thy, _) =>
       let val thy' = thy
-        |> global_theory_group
+        |> Sign.new_group
+        |> Theory.checkpoint
         |> f int
         |> Sign.reset_group;
       in Theory (Context.Theory thy', NONE) end
@@ -478,9 +486,11 @@
 fun local_theory_presentation loc f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
-          val (finish, lthy) = loc_begin loc gthy;
+          val (finish, lthy) = gthy
+            |> begin_proofs
+            |> loc_begin loc;
           val lthy' = lthy
-            |> local_theory_group
+            |> Local_Theory.new_group
             |> f int
             |> Local_Theory.reset_group;
         in Theory (finish lthy', SOME lthy') end
@@ -534,15 +544,19 @@
 
 fun local_theory_to_proof' loc f = begin_proof
   (fn int => fn gthy =>
-    let val (finish, lthy) = loc_begin loc gthy
-    in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end);
+    let val (finish, lthy) = gthy
+      |> begin_proofs
+      |> loc_begin loc;
+    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
     (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
-      (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)));
+      (case begin_proofs gthy of
+        Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
+      | _ => raise UNDEF)));
 
 end;
 
@@ -552,12 +566,12 @@
     | _ => raise UNDEF));
 
 val present_proof = present_transaction (fn _ =>
-  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
 fun proofs' f = transaction (fn int =>
-  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -357,15 +357,12 @@
   is_some (Exn.get_res (Exn.capture (fn () =>
     fst (fst (Command.memo_result (the (get_result node))))
     |> Toplevel.end_theory Position.none
-    |> Global_Theory.join_proofs) ()));
+    |> Thm.join_theory_proofs) ()));
 
 fun stable_command exec =
   (case Exn.capture Command.memo_result exec of
     Exn.Exn exn => not (Exn.is_interrupt exn)
-  | Exn.Res ((st, _), _) =>
-      (case try Toplevel.theory_of st of
-        NONE => true
-      | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
+  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
 
 fun make_required nodes =
   let
diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -89,6 +89,7 @@
   val acceptedN: string val accepted: Markup.T
   val forkedN: string val forked: Markup.T
   val joinedN: string val joined: Markup.T
+  val cancelledN: string val cancelled: Markup.T
   val failedN: string val failed: Markup.T
   val finishedN: string val finished: Markup.T
   val serialN: string
@@ -273,7 +274,7 @@
 val (acceptedN, accepted) = markup_elem "accepted";
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
-
+val (cancelledN, cancelled) = markup_elem "cancelled";
 val (failedN, failed) = markup_elem "failed";
 val (finishedN, finished) = markup_elem "finished";
 
diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 30 22:38:12 2012 +0200
@@ -195,6 +195,7 @@
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
+  val CANCELLED = "cancelled"
   val FAILED = "failed"
   val FINISHED = "finished"
 
diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Aug 30 22:38:12 2012 +0200
@@ -65,13 +65,14 @@
 
   val command_status_markup: Set[String] =
     Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
-      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
+      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
 
   def command_status(status: Status, markup: Markup): Status =
     markup match {
       case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
       case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
       case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
+      case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true)
       case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
       case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
       case _ => status
diff -r b77e1910af8a -r 8e124393c281 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -176,7 +176,7 @@
 local
 
 fun finish_thy ((thy, present, commit): result) =
-  (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
+  (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
 
 val schedule_seq =
   Graph.schedule (fn deps => fn (_, task) =>
diff -r b77e1910af8a -r 8e124393c281 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/global_theory.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -10,9 +10,6 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val begin_recent_proofs: theory -> theory
-  val join_recent_proofs: theory -> unit
-  val join_proofs: theory -> unit
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
@@ -49,42 +46,20 @@
 
 (** theory data **)
 
-type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
-
-val empty_proofs: proofs = ([], Lazy.value ());
-
-fun add_proofs more_thms ((thms, _): proofs) =
-  let val thms' = fold cons more_thms thms
-  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
-
-fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
-
 structure Data = Theory_Data
 (
-  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
-  val empty = (Facts.empty, (empty_proofs, empty_proofs));
-  fun extend (facts, _) = (facts, snd empty);
-  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
+  type T = Facts.T;
+  val empty = Facts.empty;
+  val extend = I;
+  val merge = Facts.merge;
 );
 
-
-(* facts *)
-
-val facts_of = #1 o Data.get;
+val facts_of = Data.get;
 
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;
 
-fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
-
-
-(* forked proofs *)
-
-fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
-
-val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
-val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
-val join_proofs = force_proofs o #2 o #2 o Data.get;
+fun hide_fact fully name = Data.map (Facts.hide fully name);
 
 
 (** retrieve theorems **)
@@ -149,6 +124,8 @@
 
 (* enter_thms *)
 
+fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy);
+
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
   then app_att thms thy |-> register_proofs
@@ -157,8 +134,7 @@
       val name = Sign.full_name thy b;
       val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
       val thms'' = map (Thm.transfer thy') thms';
-      val thy'' = thy'
-        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
+      val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
     in (thms'', thy'') end;
 
 
@@ -192,7 +168,7 @@
 (* add_thms_dynamic *)
 
 fun add_thms_dynamic (b, f) thy = thy
-  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
+  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
 
 
 (* note_thmss *)
diff -r b77e1910af8a -r 8e124393c281 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/goal.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -26,8 +26,9 @@
   val norm_result: thm -> thm
   val fork_name: string -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
+  val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
-  val local_future_enabled: unit -> bool
+  val future_enabled_nested: int -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -119,6 +120,24 @@
           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
     in n end);
 
+fun capture_status e =
+  let
+    val task_props =
+      (case Future.worker_task () of
+        NONE => I
+      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
+    fun status m = Output.status (Markup.markup_only (task_props m));
+
+    val _ = status Isabelle_Markup.forked;
+    val result = Exn.capture (Future.interruptible_task e) ();
+    val _ =
+      (case result of
+        Exn.Res _ => status Isabelle_Markup.joined
+      | Exn.Exn exn =>
+          if Exn.is_interrupt exn then status Isabelle_Markup.cancelled
+          else status Isabelle_Markup.failed);
+  in result end;
+
 fun fork_name name e =
   uninterruptible (fn _ => fn () =>
     let
@@ -126,9 +145,7 @@
       val future =
         (singleton o Future.forks)
           {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
-          (fn () =>
-            Exn.release
-              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
+          (fn () => Exn.release (capture_status e before forked ~1));
     in future end) ();
 
 fun fork e = fork_name "Goal.fork" e;
@@ -139,12 +156,14 @@
 val parallel_proofs = Unsynchronized.ref 1;
 val parallel_proofs_threshold = Unsynchronized.ref 50;
 
-fun future_enabled () =
-  Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
+fun future_enabled_level n =
+  Multithreading.enabled () andalso ! parallel_proofs >= n andalso
   is_some (Future.worker_task ());
 
-fun local_future_enabled () =
-  future_enabled () andalso ! parallel_proofs >= 2 andalso
+fun future_enabled () = future_enabled_level 1;
+
+fun future_enabled_nested n =
+  future_enabled_level n andalso
   Synchronized.value forked_proofs <
     ! parallel_proofs_threshold * Multithreading.max_threads_value ();
 
diff -r b77e1910af8a -r 8e124393c281 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/more_thm.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -95,6 +95,11 @@
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
+  val register_proofs: thm list -> Context.generic -> Context.generic
+  val begin_proofs: Context.generic -> Context.generic
+  val join_local_proofs: Proof.context -> unit
+  val join_recent_proofs: theory -> unit
+  val join_theory_proofs: theory -> unit
 end;
 
 structure Thm: THM =
@@ -466,6 +471,34 @@
 fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
 
 
+(* forked proofs *)
+
+type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
+
+val empty_proofs: proofs = ([], Lazy.value ());
+
+fun add_proofs more_thms ((thms, _): proofs) =
+  let val thms' = fold cons more_thms thms
+  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
+
+fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
+
+structure Proofs = Generic_Data
+(
+  type T = proofs * proofs;  (*recent proofs since last begin, all proofs of theory node*)
+  val empty = (empty_proofs, empty_proofs);
+  fun extend _ = empty;
+  fun merge _ = empty;
+);
+
+val begin_proofs = Proofs.map (apfst (K empty_proofs));
+val register_proofs = Proofs.map o pairself o add_proofs;
+
+val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
+val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
+val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
+
+
 open Thm;
 
 end;
diff -r b77e1910af8a -r 8e124393c281 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/thm.ML	Thu Aug 30 22:38:12 2012 +0200
@@ -514,7 +514,7 @@
 
 fun join_promises [] = ()
   | join_promises promises = join_promises_of (Future.joins (map snd promises))
-and join_promises_of thms = join_promises (maps raw_promises_of thms);
+and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body