# HG changeset patch
# User haftmann
# Date 1623261861 0
# Node ID bfce186331be77a93a3c0d3ccb19e100a344db1c
# Parent  8a9fd2ffb81db7c042dab411014da39891df214e
more succint interfaces

diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/class.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -493,7 +493,7 @@
     val add_dependency =
       (case some_dep_morph of
         SOME dep_morph =>
-          Locale.add_dependency sub
+          Generic_Target.locale_dependency sub
             {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
               mixin = NONE, export = export}
       | NONE => I);
@@ -667,7 +667,7 @@
 
 fun registration thy_ctxt {inst, mixin, export} lthy =
   lthy
-  |> Locale.add_registration_theory
+  |> Generic_Target.theory_registration
       {inst = inst,
        mixin = mixin,
        export = export $> Proof_Context.export_morphism lthy thy_ctxt}
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -331,10 +331,10 @@
     |-> (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'
+       Context.theory_map (Locale.add_registration
          {inst = (class, base_morph),
            mixin = Option.map (rpair true) eq_morph,
-           export = export_morph}
+           export = export_morph})
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -29,6 +29,8 @@
     (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
+  val local_interpretation: Locale.registration ->
+    local_theory -> local_theory
 
   (*lifting target primitives to local theory operations*)
   val define: (((binding * typ) * mixfix) * (binding * term) ->
@@ -54,6 +56,7 @@
   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 ->
@@ -71,6 +74,8 @@
     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
 end
 
 structure Generic_Target: GENERIC_TARGET =
@@ -230,6 +235,14 @@
 fun standard_const pred prmode ((b, mx), rhs) =
   standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
 
+fun local_interpretation registration lthy =
+  let val n = Local_Theory.level lthy in
+    lthy
+    |> Local_Theory.map_contexts (fn level =>
+      level = n - 1 ? Context.proof_map (Locale.add_registration registration))
+  end;
+
+
 
 (** lifting target primitives to local theory operations **)
 
@@ -393,6 +406,8 @@
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
 
+val theory_registration = Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
+
 
 (** locale target primitives **)
 
@@ -424,6 +439,10 @@
   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 loc registration =
+  Local_Theory.raw_theory (Locale.add_dependency loc registration)
+  #> local_interpretation registration;
+
 
 (** locale abbreviations **)
 
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/interpretation.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -140,11 +140,16 @@
     (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     "interpret" propss eqns goal_ctxt state;
 
+fun add_registration_proof registration ctxt = ctxt
+  |> Proof_Context.set_stmt false
+  |> Context.proof_map (Locale.add_registration registration)
+  |> Proof_Context.restore_stmt ctxt;
+
 fun gen_interpret prep_interpretation expression state =
   Proof.assert_forward_or_chain state
   |> Proof.context_of
   |> generic_interpretation prep_interpretation (setup_proof state)
-    Attrib.local_notes Locale.add_registration_proof expression [];
+    Attrib.local_notes add_registration_proof expression [];
 
 in
 
@@ -157,7 +162,7 @@
 (* interpretation in local theories *)
 
 val add_registration_local_theory =
-  Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+  Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation;
 
 fun interpretation expression =
   generic_interpretation cert_interpretation Element.witness_proof_eqs
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -79,13 +79,8 @@
   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_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 -> local_theory -> local_theory
+  val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
   val get_locales: theory -> string list
@@ -611,21 +606,6 @@
       |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
   end;
 
-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_proof registration ctxt = ctxt
-  |> Proof_Context.set_stmt false
-  |> Context.proof_map (add_registration registration)
-  |> Proof_Context.restore_stmt ctxt;
 
 
 (*** Dependencies ***)
@@ -637,7 +617,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 =
@@ -649,13 +629,10 @@
       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 => Context.theory_map (add_registration {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 ***)
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Jun 09 18:04:21 2021 +0000
@@ -94,7 +94,7 @@
        notes = Generic_Target.notes Generic_Target.theory_target_notes,
        abbrev = Generic_Target.theory_abbrev,
        declaration = fn _ => Generic_Target.theory_declaration,
-       theory_registration = Locale.add_registration_theory,
+       theory_registration = Generic_Target.theory_registration,
        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))]]}
@@ -104,7 +104,7 @@
        abbrev = Generic_Target.locale_abbrev locale,
        declaration = Generic_Target.locale_declaration locale,
        theory_registration = fn _ => error "Not possible in locale target",
-       locale_dependency = Locale.add_dependency locale,
+       locale_dependency = Generic_Target.locale_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),
@@ -112,7 +112,7 @@
        abbrev = Class.abbrev class,
        declaration = Generic_Target.locale_declaration class,
        theory_registration = fn _ => error "Not possible in class target",
-       locale_dependency = Locale.add_dependency class,
+       locale_dependency = Generic_Target.locale_dependency class,
        pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
 
 fun setup_context Theory = Proof_Context.init_global
diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Jun 09 11:25:21 2021 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Jun 09 18:04:21 2021 +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 = Locale.add_registration_theory,
+        theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in overloading target",
         pretty = pretty}
   end;