# HG changeset patch # User haftmann # Date 1608370391 0 # Node ID 90ada01470cbd6ef6e2ca160c541b094704c230b # Parent 09479be1fe2ad4da40d97af100b7f38d759c9312 clarified scope of concept diff -r 09479be1fe2a -r 90ada01470cb src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Fri Dec 18 10:37:26 2020 +0000 +++ b/src/Pure/Isar/interpretation.ML Sat Dec 19 09:33:11 2020 +0000 @@ -156,13 +156,16 @@ (* interpretation in local theories *) +val add_registration_local_theory = + Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory; + fun interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs - Local_Theory.notes_kind Locale.add_registration_local_theory expression []; + Local_Theory.notes_kind add_registration_local_theory expression []; fun interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs - Local_Theory.notes_kind Locale.add_registration_local_theory expression []; + Local_Theory.notes_kind add_registration_local_theory expression []; (* interpretation into global theories *) @@ -219,7 +222,7 @@ fun register_or_activate lthy = if Named_Target.is_theory lthy then Local_Theory.theory_registration - else Locale.add_registration_local_theory; + else add_registration_local_theory; fun gen_isar_interpretation prep_interpretation expression lthy = generic_interpretation prep_interpretation Element.witness_proof_eqs diff -r 09479be1fe2a -r 90ada01470cb src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Dec 18 10:37:26 2020 +0000 +++ b/src/Pure/Isar/local_theory.ML Sat Dec 19 09:33:11 2020 +0000 @@ -24,7 +24,6 @@ type operations val assert: local_theory -> local_theory val level: Proof.context -> int - val revoke_reinitializability: local_theory -> local_theory val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory val background_naming_of: local_theory -> Name_Space.naming val map_background_naming: (Name_Space.naming -> Name_Space.naming) -> @@ -69,7 +68,6 @@ conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory - val exit_global_reinitializable: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory val begin_nested: local_theory -> Binding.scope * local_theory @@ -105,12 +103,11 @@ {background_naming: Name_Space.naming, operations: operations, conclude: Proof.context -> Proof.context, - reinitializable: bool, target: Proof.context}; -fun make_lthy (background_naming, operations, conclude, reinitializable, target) : lthy = +fun make_lthy (background_naming, operations, conclude, target) : lthy = {background_naming = background_naming, operations = operations, - conclude = conclude, reinitializable = reinitializable, target = target}; + conclude = conclude, target = target}; (* context data *) @@ -150,16 +147,16 @@ fun map_top f = assert #> - Data.map (fn {background_naming, operations, conclude, reinitializable, target} :: parents => - make_lthy (f (background_naming, operations, conclude, reinitializable, target)) :: parents); + Data.map (fn {background_naming, operations, conclude, target} :: parents => + make_lthy (f (background_naming, operations, conclude, target)) :: parents); fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); fun map_contexts f lthy = let val n = level lthy in lthy |> (Data.map o map_index) - (fn (i, {background_naming, operations, conclude, reinitializable, target}) => - make_lthy (background_naming, operations, conclude, reinitializable, + (fn (i, {background_naming, operations, conclude, target}) => + make_lthy (background_naming, operations, conclude, target |> Context_Position.set_visible false |> f (n - i - 1) @@ -168,26 +165,13 @@ end; -(* reinitializable context -- implicit for nested structures *) - -fun revoke_reinitializability lthy = - if level lthy = 1 then - map_top (fn (background_naming, operations, conclude, _, target) => - (background_naming, operations, conclude, false, target)) lthy - else lthy; - -fun assert_reinitializable lthy = - if #reinitializable (top_of lthy) then lthy - else error "Non-reinitializable local theory context"; - - (* naming for background theory *) val background_naming_of = #background_naming o top_of; fun map_background_naming f = - map_top (fn (background_naming, operations, conclude, reinitializable, target) => - (f background_naming, operations, conclude, reinitializable, target)); + map_top (fn (background_naming, operations, conclude, target) => + (f background_naming, operations, conclude, target)); val restore_background_naming = map_background_naming o K o background_naming_of; @@ -353,8 +337,7 @@ (* main target *) fun init_target background_naming conclude operations target = - Data.map (K [make_lthy - (background_naming, operations, conclude, true, target)]) target + Data.map (K [make_lthy (background_naming, operations, conclude, target)]) target fun init {background_naming, setup, conclude} operations thy = thy @@ -366,7 +349,6 @@ fun exit lthy = exit_of lthy (assert_bottom lthy); val exit_global = Proof_Context.theory_of o exit; -val exit_global_reinitializable = exit_global o assert_reinitializable; fun exit_result decl (x, lthy) = let @@ -389,7 +371,7 @@ val _ = assert lthy; val (scope, target) = Proof_Context.new_scope lthy; val entry = make_lthy (background_naming_of lthy, operations_of lthy, - Proof_Context.restore_naming lthy, true, target); + Proof_Context.restore_naming lthy, target); val lthy' = Data.map (cons entry) target; in (scope, lthy') end; diff -r 09479be1fe2a -r 90ada01470cb src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Dec 18 10:37:26 2020 +0000 +++ b/src/Pure/Isar/locale.ML Sat Dec 19 09:33:11 2020 +0000 @@ -615,16 +615,13 @@ val add_registration_theory = Local_Theory.raw_theory o add_registration_theory'; -fun add_registration_local_theory' registration lthy = +fun add_registration_local_theory registration lthy = let val n = Local_Theory.level lthy in lthy |> Local_Theory.map_contexts (fn level => level = n - 1 ? Context.proof_map (add_registration registration)) end; -fun add_registration_local_theory registration = - Local_Theory.revoke_reinitializability #> add_registration_local_theory' registration - fun add_registration_proof registration ctxt = ctxt |> Proof_Context.set_stmt false |> Context.proof_map (add_registration registration) @@ -658,7 +655,7 @@ fun add_dependency loc registration = Local_Theory.raw_theory (add_dependency' loc registration) - #> add_registration_local_theory' registration; + #> add_registration_local_theory registration; (*** Storing results ***) diff -r 09479be1fe2a -r 90ada01470cb src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Fri Dec 18 10:37:26 2020 +0000 +++ b/src/Pure/Isar/named_target.ML Sat Dec 19 09:33:11 2020 +0000 @@ -16,7 +16,8 @@ val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory - val reinit: local_theory -> theory -> local_theory + val revoke_reinitializability: local_theory -> local_theory + val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory end; structure Named_Target: NAMED_TARGET = @@ -48,11 +49,11 @@ structure Data = Proof_Data ( - type T = target option; + type T = (target * bool) option; fun init _ = NONE; ); -val get_bottom_target = Data.get; +val get_bottom_target = Option.map fst o Data.get; fun get_target lthy = if Local_Theory.level lthy = 1 @@ -72,6 +73,9 @@ val class_of = class_of_target o get_target; +fun is_reinitializable lthy = + Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy; + (* operations *) @@ -115,6 +119,11 @@ | setup_context (Locale locale) = Locale.init locale | setup_context (Class class) = Class.init class; +fun setup target includes = + setup_context target + #> Data.put (SOME (target, null includes)) + #> Bundle.includes includes; + fun init includes ident thy = let val target = target_of_ident thy ident; @@ -122,10 +131,9 @@ thy |> Local_Theory.init {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), - setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes, + setup = setup target includes, conclude = I} (operations target) - |> not (null includes) ? Local_Theory.revoke_reinitializability end; val theory_init = init [] ""; @@ -134,6 +142,11 @@ fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; -fun reinit lthy = init [] (ident_of lthy); +val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); + +fun exit_global_reinitialize lthy = + if is_reinitializable lthy + then (init [] (ident_of lthy), Local_Theory.exit_global lthy) + else error "Non-reinitializable local theory context"; end; diff -r 09479be1fe2a -r 90ada01470cb src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML Fri Dec 18 10:37:26 2020 +0000 +++ b/src/Pure/Isar/target_context.ML Sat Dec 19 09:33:11 2020 +0000 @@ -36,8 +36,12 @@ | switch_named_cmd NONE (Context.Proof lthy) = (Context.Proof o Local_Theory.reset, lthy) | switch_named_cmd (SOME name) (Context.Proof lthy) = - (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, - (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy); + let + val (reinit, thy) = Named_Target.exit_global_reinitialize lthy + in + (Context.Proof o reinit o Local_Theory.exit_global, + context_begin_named_cmd [] name thy) + end; fun includes raw_includes lthy = Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;