# HG changeset patch # User haftmann # Date 1608287846 0 # Node ID 09479be1fe2ad4da40d97af100b7f38d759c9312 # Parent 74339f1a5dd792d1c69fdcf43d69ba67518d50f7 clarified name diff -r 74339f1a5dd7 -r 09479be1fe2a src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Dec 19 00:23:21 2020 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Dec 18 10:37:26 2020 +0000 @@ -24,7 +24,7 @@ type operations val assert: local_theory -> local_theory val level: Proof.context -> int - val mark_brittle: local_theory -> local_theory + 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 +69,7 @@ conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory - val exit_global_nonbrittle: 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 +105,12 @@ {background_naming: Name_Space.naming, operations: operations, conclude: Proof.context -> Proof.context, - brittle: bool, + reinitializable: bool, target: Proof.context}; -fun make_lthy (background_naming, operations, conclude, brittle, target) : lthy = +fun make_lthy (background_naming, operations, conclude, reinitializable, target) : lthy = {background_naming = background_naming, operations = operations, - conclude = conclude, brittle = brittle, target = target}; + conclude = conclude, reinitializable = reinitializable, target = target}; (* context data *) @@ -150,16 +150,16 @@ fun map_top f = assert #> - Data.map (fn {background_naming, operations, conclude, brittle, target} :: parents => - make_lthy (f (background_naming, operations, conclude, brittle, target)) :: parents); + Data.map (fn {background_naming, operations, conclude, reinitializable, target} :: parents => + make_lthy (f (background_naming, operations, conclude, reinitializable, 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, brittle, target}) => - make_lthy (background_naming, operations, conclude, brittle, + (fn (i, {background_naming, operations, conclude, reinitializable, target}) => + make_lthy (background_naming, operations, conclude, reinitializable, target |> Context_Position.set_visible false |> f (n - i - 1) @@ -168,17 +168,17 @@ end; -(* brittle context -- implicit for nested structures *) +(* reinitializable context -- implicit for nested structures *) -fun mark_brittle lthy = +fun revoke_reinitializability lthy = if level lthy = 1 then map_top (fn (background_naming, operations, conclude, _, target) => - (background_naming, operations, conclude, true, target)) lthy + (background_naming, operations, conclude, false, target)) lthy else lthy; -fun assert_nonbrittle lthy = - if #brittle (top_of lthy) then error "Brittle local theory context" - else lthy; +fun assert_reinitializable lthy = + if #reinitializable (top_of lthy) then lthy + else error "Non-reinitializable local theory context"; (* naming for background theory *) @@ -186,8 +186,8 @@ val background_naming_of = #background_naming o top_of; fun map_background_naming f = - map_top (fn (background_naming, operations, conclude, brittle, target) => - (f background_naming, operations, conclude, brittle, target)); + map_top (fn (background_naming, operations, conclude, reinitializable, target) => + (f background_naming, operations, conclude, reinitializable, target)); val restore_background_naming = map_background_naming o K o background_naming_of; @@ -354,7 +354,7 @@ fun init_target background_naming conclude operations target = Data.map (K [make_lthy - (background_naming, operations, conclude, false, target)]) target + (background_naming, operations, conclude, true, target)]) target fun init {background_naming, setup, conclude} operations thy = thy @@ -366,7 +366,7 @@ fun exit lthy = exit_of lthy (assert_bottom lthy); val exit_global = Proof_Context.theory_of o exit; -val exit_global_nonbrittle = exit_global o assert_nonbrittle; +val exit_global_reinitializable = exit_global o assert_reinitializable; fun exit_result decl (x, lthy) = let diff -r 74339f1a5dd7 -r 09479be1fe2a src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Dec 19 00:23:21 2020 +0100 +++ b/src/Pure/Isar/locale.ML Fri Dec 18 10:37:26 2020 +0000 @@ -623,7 +623,7 @@ end; fun add_registration_local_theory registration = - Local_Theory.mark_brittle #> 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 diff -r 74339f1a5dd7 -r 09479be1fe2a src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Sat Dec 19 00:23:21 2020 +0100 +++ b/src/Pure/Isar/named_target.ML Fri Dec 18 10:37:26 2020 +0000 @@ -125,7 +125,7 @@ setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes, conclude = I} (operations target) - |> not (null includes) ? Local_Theory.mark_brittle + |> not (null includes) ? Local_Theory.revoke_reinitializability end; val theory_init = init [] ""; diff -r 74339f1a5dd7 -r 09479be1fe2a src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML Sat Dec 19 00:23:21 2020 +0100 +++ b/src/Pure/Isar/target_context.ML Fri Dec 18 10:37:26 2020 +0000 @@ -37,7 +37,7 @@ (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_nonbrittle) lthy); + (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy); fun includes raw_includes lthy = Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;