refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;

--- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 21:23:04 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;

--- a/src/Pure/Isar/proof.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 30 21:23:04 2012 +0200
@@ -1137,19 +1137,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;
 

--- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 21:23:04 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 #>
-  Context.theory_map Thm.begin_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 (Context.theory_map Thm.begin_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));
 

--- a/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 30 21:23:04 2012 +0200
@@ -362,10 +362,7 @@
 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 Thm.join_recent_proofs thy))));
+  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
 
 fun make_required nodes =
   let

--- a/src/Pure/goal.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/goal.ML	Thu Aug 30 21:23:04 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 ->
@@ -155,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 ();