# HG changeset patch # User wenzelm # Date 1457178587 -3600 # Node ID aae510e9a698c3fd494ee71459413d9297e53a20 # Parent 702085ca85648014ef4b57699fb772c7bc9892db tuned signature; diff -r 702085ca8564 -r aae510e9a698 NEWS --- a/NEWS Fri Feb 26 22:38:44 2016 +0100 +++ b/NEWS Sat Mar 05 12:49:47 2016 +0100 @@ -189,6 +189,14 @@ debugger information requires consirable time and space: main Isabelle/HOL with full debugger support may need ML_system_64. +* Local_Theory.restore has been renamed to Local_Theory.reset to +emphasize its disruptive impact on the cumulative context, notably the +scope of 'private' or 'qualified' names. Note that Local_Theory.reset is +only appropriate when targets are managed, e.g. starting from a global +theory and returning to it. Regular definitional packages should use +balanced blocks of Local_Theory.open_target versus +Local_Theory.close_target instead. Rare INCOMPATIBILITY. + *** System *** diff -r 702085ca8564 -r aae510e9a698 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/HOL/Library/bnf_axiomatization.ML Sat Mar 05 12:49:47 2016 +0100 @@ -83,7 +83,7 @@ val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy - ||> `Local_Theory.restore; + ||> `Local_Theory.reset; fun mk_wit_thms set_maps = Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) diff -r 702085ca8564 -r aae510e9a698 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Sat Mar 05 12:49:47 2016 +0100 @@ -610,7 +610,7 @@ lthy |> Local_Theory.notes (notes (#notes config)) |> snd |> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) - ||> Local_Theory.restore + ||> Local_Theory.reset end (* This is not very cheap way of getting the rules but we have only few active diff -r 702085ca8564 -r aae510e9a698 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Mar 05 12:49:47 2016 +0100 @@ -211,7 +211,7 @@ handle THM _ => error ("code_dt: " ^ quote (Tname qty) ^ " was not defined as a subtype.")) val code_dt = mk_code_dt rty qty wit wit_thm NONE in - (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.restore, rel_eq_onps)) + (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.reset, rel_eq_onps)) end else (quot_thm, (lthy, rel_eq_onps)) @@ -340,7 +340,7 @@ val lthy = lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context) - |> Local_Theory.restore + |> Local_Theory.reset (* in order to make the qty qty_isom isomorphism executable we have to define discriminators and selectors for qty_isom *) @@ -571,12 +571,12 @@ val config = { notes = false} val (binding, lthy) = conceal_naming_result (Lifting_Setup.setup_by_typedef_thm config type_definition_thm) lthy - val lthy = Local_Theory.restore lthy + val lthy = Local_Theory.reset lthy val (wit, wit_thm) = mk_witness quot_thm; val code_dt = mk_code_dt rty qty wit wit_thm NONE; val lthy = lthy |> update_code_dt code_dt - |> Local_Theory.restore + |> Local_Theory.reset |> mk_rep_isom binding (rty, qty, qty_isom) |> snd in (quot_thm, (lthy, rel_eq_onps)) diff -r 702085ca8564 -r aae510e9a698 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sat Mar 05 12:49:47 2016 +0100 @@ -215,7 +215,7 @@ |> snd |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) - |> Local_Theory.restore + |> Local_Theory.reset end (* BNF interpretation *) @@ -268,7 +268,7 @@ lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) - |> Local_Theory.restore + |> Local_Theory.reset end fun transfer_fp_sugars_interpretation fp_sugar lthy = diff -r 702085ca8564 -r aae510e9a698 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/Pure/Isar/local_theory.ML Sat Mar 05 12:49:47 2016 +0100 @@ -16,7 +16,7 @@ sig type operations val assert: local_theory -> local_theory - val restore: local_theory -> local_theory + val reset: local_theory -> local_theory val level: Proof.context -> int val assert_bottom: bool -> local_theory -> local_theory val mark_brittle: local_theory -> local_theory @@ -132,7 +132,7 @@ Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents => make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents); -fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy); +fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); (* nested structure *) @@ -388,6 +388,6 @@ let val _ = assert_bottom false lthy; val ({after_close, ...} :: rest) = Data.get lthy; - in lthy |> Data.put rest |> restore |> after_close end; + in lthy |> Data.put rest |> reset |> after_close end; end; diff -r 702085ca8564 -r aae510e9a698 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Fri Feb 26 22:38:44 2016 +0100 +++ b/src/Pure/Isar/named_target.ML Sat Mar 05 12:49:47 2016 +0100 @@ -176,7 +176,7 @@ | switch (SOME name) (Context.Theory thy) = (Context.Theory o exit, begin name thy) | switch NONE (Context.Proof lthy) = - (Context.Proof o Local_Theory.restore, lthy) + (Context.Proof o Local_Theory.reset, lthy) | switch (SOME name) (Context.Proof lthy) = (Context.Proof o init (target_of lthy) o exit, (begin name o exit o Local_Theory.assert_nonbrittle) lthy);