more precise register_proofs for local goals;
authorwenzelm
Fri Aug 31 16:35:30 2012 +0200 (2012-08-31 ago)
changeset 4904201041f7bf9b4
parent 49041 9edfd36a0355
child 49058 2924a83a4a0b
more precise register_proofs for local goals;
tuned signature;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Aug 31 15:25:26 2012 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Aug 31 16:35:30 2012 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     1.5    val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     1.6    val background_theory: (theory -> theory) -> local_theory -> local_theory
     1.7 +  val begin_proofs: local_theory -> local_theory
     1.8 +  val register_proofs: thm list -> local_theory -> local_theory
     1.9    val target_of: local_theory -> Proof.context
    1.10    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    1.11    val target_morphism: local_theory -> morphism
    1.12 @@ -190,6 +192,12 @@
    1.13  fun background_theory f = #2 o background_theory_result (f #> pair ());
    1.14  
    1.15  
    1.16 +(* forked proofs *)
    1.17 +
    1.18 +val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs);
    1.19 +val register_proofs = background_theory o Context.theory_map o Thm.register_proofs;
    1.20 +
    1.21 +
    1.22  (* target contexts *)
    1.23  
    1.24  val target_of = #target o get_last_lthy;
     2.1 --- a/src/Pure/Isar/proof.ML	Fri Aug 31 15:25:26 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Fri Aug 31 16:35:30 2012 +0200
     2.3 @@ -78,15 +78,15 @@
     2.4    val begin_block: state -> state
     2.5    val next_block: state -> state
     2.6    val end_block: state -> state
     2.7 -  val begin_notepad: Proof.context -> state
     2.8 -  val end_notepad: state -> Proof.context
     2.9 +  val begin_notepad: context -> state
    2.10 +  val end_notepad: state -> context
    2.11    val proof: Method.text option -> state -> state Seq.seq
    2.12    val defer: int option -> state -> state Seq.seq
    2.13    val prefer: int -> state -> state Seq.seq
    2.14    val apply: Method.text -> state -> state Seq.seq
    2.15    val apply_end: Method.text -> state -> state Seq.seq
    2.16    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    2.17 -    (Proof.context -> 'a -> attribute) ->
    2.18 +    (context -> 'a -> attribute) ->
    2.19      ('b list -> context -> (term list list * (context -> context)) * context) ->
    2.20      string -> Method.text option -> (thm list list -> state -> state) ->
    2.21      ((binding * 'a list) * 'b) list -> state -> state
    2.22 @@ -116,7 +116,7 @@
    2.23      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
    2.24    val schematic_goal: state -> bool
    2.25    val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
    2.26 -  val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
    2.27 +  val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
    2.28    val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
    2.29    val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
    2.30  end;
    2.31 @@ -939,7 +939,6 @@
    2.32        |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
    2.33    in
    2.34      outer_state
    2.35 -    |> register_proofs (flat results)
    2.36      |> map_context (after_ctxt props)
    2.37      |> pair (after_qed, results)
    2.38    end;
    2.39 @@ -967,7 +966,7 @@
    2.40  fun local_qeds txt =
    2.41    end_proof false txt
    2.42    #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
    2.43 -    (fn ((after_qed, _), results) => after_qed results));
    2.44 +    (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results));
    2.45  
    2.46  fun local_qed txt = local_qeds txt #> check_finish;
    2.47  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Fri Aug 31 15:25:26 2012 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Aug 31 16:35:30 2012 +0200
     3.3 @@ -425,8 +425,9 @@
     3.4  
     3.5  (* forked proofs *)
     3.6  
     3.7 -val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
     3.8 -val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
     3.9 +val begin_proofs =
    3.10 +  Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint)
    3.11 +    Local_Theory.begin_proofs;
    3.12  
    3.13  fun join_recent_proofs st =
    3.14    (case try proof_of st of