clarified scope of concept

--- 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

--- 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;
 

--- 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 ***)

--- 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;

--- 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;