# HG changeset patch # User wenzelm # Date 1346521398 -7200 # Node ID 7e31dfd99ce7cff2737d24d33fad9d885b6f6b42 # Parent 7449b804073bab208fa3bc7e09dbef900df70743 discontinued complicated/unreliable notion of recent proofs within context; diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/Isar/local_theory.ML Sat Sep 01 19:43:18 2012 +0200 @@ -30,8 +30,6 @@ val raw_theory: (theory -> theory) -> local_theory -> local_theory val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val background_theory: (theory -> theory) -> local_theory -> local_theory - val begin_proofs: local_theory -> local_theory - val register_proofs: thm list -> local_theory -> local_theory val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism @@ -192,12 +190,6 @@ fun background_theory f = #2 o background_theory_result (f #> pair ()); -(* forked proofs *) - -val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs); -val register_proofs = background_theory o Thm.register_proofs_thy; - - (* target contexts *) val target_of = #target o get_last_lthy; diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/Isar/proof.ML Sat Sep 01 19:43:18 2012 +0200 @@ -21,9 +21,6 @@ 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 @@ -225,14 +222,6 @@ 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; @@ -966,7 +955,7 @@ fun local_qeds txt = end_proof false txt #> Seq.map (generic_qed Proof_Context.auto_bind_facts #-> - (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results)); + (fn ((after_qed, _), results) => after_qed results)); fun local_qed txt = local_qeds txt #> check_finish; diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/Isar/specification.ML Sat Sep 01 19:43:18 2012 +0200 @@ -395,8 +395,7 @@ let val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results; val (res, lthy') = - if forall (Attrib.is_empty_binding o fst) stmt - then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy) + if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy) else Local_Theory.notes_kind kind (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Sat Sep 01 19:43:18 2012 +0200 @@ -53,7 +53,6 @@ val ignored: Position.T -> transition val malformed: Position.T -> string -> transition val is_malformed: transition -> bool - 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 @@ -423,21 +422,6 @@ val unknown_context = imperative (fn () => warning "Unknown context"); -(* forked proofs *) - -val begin_proofs = - Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint) - Local_Theory.begin_proofs; - -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 => ())); - - (* theory transitions *) fun generic_theory f = transaction (fn _ => @@ -487,9 +471,7 @@ fun local_theory_presentation loc f = present_transaction (fn int => (fn Theory (gthy, _) => let - val (finish, lthy) = gthy - |> begin_proofs - |> loc_begin loc; + val (finish, lthy) = loc_begin loc gthy; val lthy' = lthy |> Local_Theory.new_group |> f int @@ -545,9 +527,7 @@ fun local_theory_to_proof' loc f = begin_proof (fn int => fn gthy => - let val (finish, lthy) = gthy - |> begin_proofs - |> loc_begin loc; + let val (finish, lthy) = loc_begin loc gthy 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); @@ -555,7 +535,7 @@ fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Proof_Context.theory_of, - (case begin_proofs gthy of + (case gthy of Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))); @@ -567,12 +547,12 @@ | _ => raise UNDEF)); val present_proof = present_transaction (fn _ => - (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); fun proofs' f = transaction (fn int => - (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/global_theory.ML Sat Sep 01 19:43:18 2012 +0200 @@ -124,7 +124,7 @@ (* enter_thms *) -fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy); +fun register_proofs thms thy = (thms, Thm.register_proofs thms thy); fun enter_thms pre_name post_name app_att (b, thms) thy = if Binding.is_empty b diff -r 7449b804073b -r 7e31dfd99ce7 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Sep 01 19:27:28 2012 +0200 +++ b/src/Pure/more_thm.ML Sat Sep 01 19:43:18 2012 +0200 @@ -95,11 +95,7 @@ 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 register_proofs_thy: thm list -> theory -> theory - val begin_proofs: Context.generic -> Context.generic - val join_local_proofs: Proof.context -> unit - val join_recent_proofs: theory -> unit + val register_proofs: thm list -> theory -> theory val join_theory_proofs: theory -> unit end; @@ -474,31 +470,16 @@ (* 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 +structure Proofs = Theory_Data ( - type T = proofs * proofs; (*recent proofs since last begin, all proofs of theory node*) - val empty = (empty_proofs, empty_proofs); + type T = thm list; + val empty = []; 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 register_proofs_thy = Context.theory_map o register_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; +fun register_proofs more_thms = Proofs.map (fn thms => fold cons more_thms thms); +val join_theory_proofs = Thm.join_proofs o rev o Proofs.get; open Thm;