subscription as target-specific implementation device

--- a/src/Pure/Isar/class.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Isar/class.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -585,6 +585,7 @@
         notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
+        subscription = Generic_Target.theory_registration,
         pretty = pretty,
         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;

--- a/src/Pure/Isar/expression.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -921,14 +921,9 @@
 
 (* second dimension: relation to underlying target *)
 
-fun subscribe lthy =
-  if Named_Target.is_theory lthy
-  then Generic_Target.theory_registration
-  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
-
 fun subscribe_or_activate lthy =
   if Named_Target.is_theory lthy
-  then subscribe lthy
+  then Local_Theory.subscription
   else Local_Theory.activate;
 
 fun subscribe_locale_only lthy =
@@ -937,7 +932,7 @@
       if Named_Target.is_theory lthy
       then error "Not possible on level of global theory"
       else ();
-  in subscribe lthy end;
+  in Local_Theory.subscription end;
 
 
 (* special case: global sublocale command *)
@@ -964,7 +959,7 @@
 fun interpret_cmd x = gen_interpret read_interpretation x;
 
 fun permanent_interpretation x =
-  gen_local_theory_interpretation cert_interpretation subscribe x;
+  gen_local_theory_interpretation cert_interpretation (K Local_Theory.subscription) x;
 
 fun ephemeral_interpretation x =
   gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;

--- a/src/Pure/Isar/local_theory.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -49,6 +49,8 @@
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
+  val subscription: string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
@@ -83,6 +85,8 @@
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
+  subscription: string * morphism -> (morphism * bool) option -> morphism ->
+     local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list,
   exit: local_theory -> Proof.context};
 
@@ -252,6 +256,7 @@
 
 fun operation f lthy = f (operations_of lthy) lthy;
 fun operation2 f x y = operation (fn ops => f ops x y);
+fun operation3 f x y z = operation (fn ops => f ops x y z);
 
 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
@@ -259,6 +264,7 @@
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
+val subscription = operation3 #subscription;
 
 
 (* basic derived operations *)

--- a/src/Pure/Isar/named_target.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -134,6 +134,14 @@
     |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
 
 
+(* subscription *)
+
+fun target_subscription (Target {target, ...}) =
+  if target = ""
+  then Generic_Target.theory_registration
+  else Generic_Target.locale_dependency target
+
+
 (* pretty *)
 
 fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
@@ -183,6 +191,7 @@
         notes = Generic_Target.notes (target_notes ta),
         abbrev = Generic_Target.abbrev (target_abbrev ta),
         declaration = target_declaration ta,
+        subscription = target_subscription ta,
         pretty = pretty ta,
         exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
   end;

--- a/src/Pure/Isar/overloading.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -205,6 +205,7 @@
         notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
+        subscription = Generic_Target.theory_registration,
         pretty = pretty,
         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;

--- a/src/Tools/permanent_interpretation.ML	Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML	Fri Apr 25 21:45:04 2014 +0200
@@ -85,13 +85,8 @@
 
 (* interpretation with permanent registration *)
 
-fun subscribe lthy =
-  if Named_Target.is_theory lthy
-  then Generic_Target.theory_registration
-  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
-
 fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
-  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
+  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.subscription
     expression raw_defs raw_eqns lthy
 
 in