tuned interfaces

--- a/src/Pure/Isar/class.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/class.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -493,7 +493,7 @@
     val add_dependency =
       (case some_dep_morph of
         SOME dep_morph =>
-          Generic_Target.locale_dependency sub
+          Locale.add_dependency sub
             {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
               mixin = NONE, export = export}
       | NONE => I);
@@ -710,7 +710,7 @@
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
-        theory_registration = Generic_Target.theory_registration,
+        theory_registration = Locale.add_registration_theory,
         locale_dependency = fn _ => error "Not possible in instantiation target",
         pretty = pretty}
   end;

--- a/src/Pure/Isar/class_declaration.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/class_declaration.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -327,7 +327,7 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
-       Locale.add_registration_theory
+       Locale.add_registration_theory'
          {inst = (class, base_morph),
            mixin = Option.map (rpair true) eq_morph,
            export = export_morph}

--- a/src/Pure/Isar/generic_target.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/generic_target.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -54,7 +54,6 @@
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> (term * term) * local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_registration: Locale.registration -> local_theory -> local_theory
 
   (*locale target primitives*)
   val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
@@ -72,7 +71,6 @@
     local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
-  val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
 
   (*initialisation*)
   val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -400,10 +398,6 @@
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
 
-val theory_registration =
-  Local_Theory.raw_theory o Locale.add_registration_theory;
-
-
 
 (** locale target primitives **)
 
@@ -435,10 +429,6 @@
   locale_target_const locale (K true) prmode ((b, mx), rhs)
   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
 
-fun locale_dependency locale registration =
-  Local_Theory.raw_theory (Locale.add_dependency locale registration)
-  #> Locale.add_registration_local_theory registration;
-
 
 (** locale abbreviations **)
 

--- a/src/Pure/Isar/interpretation.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/interpretation.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -156,16 +156,13 @@
 
 (* interpretation in local theories *)
 
-fun activate_fragment registration =
-  Local_Theory.mark_brittle #> Locale.add_registration_local_theory registration;
-
 fun interpretation expression =
   generic_interpretation cert_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind activate_fragment expression [];
+    Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
 
 fun interpretation_cmd expression =
   generic_interpretation read_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind activate_fragment expression [];
+    Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
 
 
 (* interpretation into global theories *)
@@ -222,7 +219,7 @@
 fun register_or_activate lthy =
   if Named_Target.is_theory lthy
   then Local_Theory.theory_registration
-  else activate_fragment;
+  else Locale.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	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -24,9 +24,7 @@
   type operations
   val assert: local_theory -> local_theory
   val level: Proof.context -> int
-  val assert_bottom: local_theory -> local_theory
   val mark_brittle: local_theory -> local_theory
-  val assert_nonbrittle: 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) ->
@@ -71,6 +69,7 @@
     operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
+  val exit_global_nonbrittle: 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
@@ -363,6 +362,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;
 
 fun exit_result decl (x, lthy) =
   let

--- a/src/Pure/Isar/locale.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/locale.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -79,11 +79,13 @@
   type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}
   val amend_registration: registration -> Context.generic -> Context.generic
   val add_registration: registration -> Context.generic -> Context.generic
-  val add_registration_theory: registration -> theory -> theory
-  val add_registration_proof: registration -> Proof.context -> Proof.context
+  val add_registration_theory': registration -> theory -> theory
+  val add_registration_theory: registration -> local_theory -> local_theory
   val add_registration_local_theory: registration -> local_theory -> local_theory
+  val add_registration_proof: registration -> Proof.context -> Proof.context
   val registrations_of: Context.generic -> string -> (string * morphism) list
-  val add_dependency: string -> registration -> theory -> theory
+  val add_dependency': string -> registration -> theory -> theory
+  val add_dependency: string -> registration -> local_theory -> local_theory
 
   (* Diagnostic *)
   val get_locales: theory -> string list
@@ -609,20 +611,25 @@
       |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
   end;
 
-val add_registration_theory = Context.theory_map o add_registration;
+val add_registration_theory' = Context.theory_map o add_registration;
+
+val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
+
+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.mark_brittle #> add_registration_local_theory' registration
 
 fun add_registration_proof registration ctxt = ctxt
   |> Proof_Context.set_stmt false
   |> Context.proof_map (add_registration registration)
   |> Proof_Context.restore_stmt ctxt;
 
-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;
-
-
 
 (*** Dependencies ***)
 
@@ -633,7 +640,7 @@
   |> map (fn (name, (base, export)) =>
       (name, base $> (collect_mixins context (name, base $> export)) $> export));
 
-fun add_dependency loc {inst = (name, morph), mixin, export} thy =
+fun add_dependency' loc {inst = (name, morph), mixin, export} thy =
   let
     val dep = make_dep (name, (morph, export));
     val add_dep =
@@ -645,10 +652,14 @@
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
   in
-    fold_rev (fn inst => add_registration_theory {inst = inst, mixin = NONE, export = export})
+    fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export})
       regs thy'
   end;
 
+fun add_dependency loc registration =
+  Local_Theory.raw_theory (add_dependency' loc registration)
+  #> add_registration_local_theory' registration;
+
 
 (*** Storing results ***)
 

--- a/src/Pure/Isar/named_target.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/named_target.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -92,7 +92,7 @@
        notes = Generic_Target.notes Generic_Target.theory_target_notes,
        abbrev = Generic_Target.theory_abbrev,
        declaration = fn _ => Generic_Target.theory_declaration,
-       theory_registration = Generic_Target.theory_registration,
+       theory_registration = Locale.add_registration_theory,
        locale_dependency = fn _ => error "Not possible in theory target",
        pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
         Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
@@ -102,7 +102,7 @@
        abbrev = Generic_Target.locale_abbrev locale,
        declaration = Generic_Target.locale_declaration locale,
        theory_registration = fn _ => error "Not possible in locale target",
-       locale_dependency = Generic_Target.locale_dependency locale,
+       locale_dependency = Locale.add_dependency locale,
        pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]}
   | operations (Class class) =
       {define = Generic_Target.define (class_foundation class),
@@ -110,7 +110,7 @@
        abbrev = Class.abbrev class,
        declaration = Generic_Target.locale_declaration class,
        theory_registration = fn _ => error "Not possible in class target",
-       locale_dependency = Generic_Target.locale_dependency class,
+       locale_dependency = Locale.add_dependency class,
        pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
 
 fun setup_context Theory = Proof_Context.init_global

--- a/src/Pure/Isar/overloading.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/overloading.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -210,7 +210,7 @@
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
-        theory_registration = Generic_Target.theory_registration,
+        theory_registration = Locale.add_registration_theory,
         locale_dependency = fn _ => error "Not possible in overloading target",
         pretty = pretty}
   end;

--- a/src/Pure/Isar/target_context.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/target_context.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -7,7 +7,7 @@
 signature TARGET_CONTEXT =
 sig
   val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
-  val end_named_cmd: local_theory -> theory
+  val end_named_cmd: local_theory -> Context.generic
   val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
     (local_theory -> Context.generic) * local_theory
   val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
@@ -21,17 +21,17 @@
 fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
   | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
 
-val end_named_cmd = Local_Theory.exit_global;
+val end_named_cmd = Context.Theory o Local_Theory.exit_global;
 
 fun switch_named_cmd NONE (Context.Theory thy) =
-      (Context.Theory o end_named_cmd, Named_Target.theory_init thy)
+      (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy)
   | switch_named_cmd (SOME name) (Context.Theory thy) =
-      (Context.Theory o end_named_cmd, context_begin_named_cmd name thy)
+      (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy)
   | 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 end_named_cmd,
-        (context_begin_named_cmd name o end_named_cmd o Local_Theory.assert_nonbrittle) 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);
 
 fun includes raw_incls lthy =
   Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
@@ -45,10 +45,14 @@
   |> Local_Theory.begin_nested
   |> snd;
 
-fun end_nested_cmd lthy = 
-  if Named_Target.is_theory lthy
-  then Context.Theory (Local_Theory.exit_global lthy)
-  else Context.Proof lthy;
+fun end_nested_cmd lthy =
+  let
+    val lthy' = Local_Theory.end_nested lthy
+  in
+    if Named_Target.is_theory lthy'
+    then Context.Theory (Local_Theory.exit_global lthy')
+    else Context.Proof lthy'
+  end;
 
 end;
 

--- a/src/Pure/Isar/toplevel.ML	Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/toplevel.ML	Sat Oct 24 15:16:54 2020 +0000
@@ -439,7 +439,7 @@
           val gthy =
             if begin
             then Context.Proof lthy
-            else Context.Theory (Target_Context.end_named_cmd lthy);
+            else Target_Context.end_named_cmd lthy;
           val _ =
             (case Local_Theory.pretty lthy of
               [] => ()
@@ -448,7 +448,7 @@
     | _ => raise UNDEF));
 
 val end_main_target = transaction (fn _ =>
-  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Target_Context.end_named_cmd lthy)), lthy)
+  (fn Theory (Context.Proof lthy) => (Theory (Target_Context.end_named_cmd lthy), lthy)
     | _ => raise UNDEF));
 
 fun begin_nested_target f = transaction0 (fn _ =>
@@ -460,10 +460,8 @@
 
 val end_nested_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) =>
-        (case try Local_Theory.end_nested lthy of
-          SOME lthy' =>
-            let val gthy' = Target_Context.end_nested_cmd lthy'
-            in (Theory gthy', lthy) end
+        (case try Target_Context.end_nested_cmd lthy of
+          SOME gthy' => (Theory gthy', lthy)
         | NONE => raise UNDEF)
     | _ => raise UNDEF));