# HG changeset patch
# User wenzelm
# Date 1346356249 -7200
# Node ID 1266b51f9bbc77e51dd7b65bae5e661b28359c62
# Parent  8686c36fa27dd08248f1f170132ab4c726de6c39
register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;

diff -r 8686c36fa27d -r 1266b51f9bbc src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Aug 30 21:23:04 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 30 21:50:49 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
@@ -111,9 +114,6 @@
     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val begin_proofs: state -> state
-  val register_proofs: thm list -> state -> state
-  val join_recent_proofs: state -> unit
   val schematic_goal: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
   val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
@@ -225,6 +225,14 @@
 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 top;
@@ -931,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;
@@ -1060,14 +1069,6 @@
 
 (** future proofs **)
 
-(* 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;
-
-
 (* relevant proof states *)
 
 fun is_schematic t =