# HG changeset patch
# User haftmann
# Date 1369590354 -7200
# Node ID f5773a46cf058afd700bb9cf761820b1979bd477
# Parent  b561cdce6c4c271dd106962da997645dd2f1d7f2
more specific structure for registration into theory and dependency onto locale

diff -r b561cdce6c4c -r f5773a46cf05 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
@@ -882,7 +882,7 @@
   then 
     lthy
     |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
+        Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
   else
     lthy
     |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
@@ -895,7 +895,7 @@
   in
     lthy
     |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
+        Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
   end;
   
 fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
@@ -915,8 +915,8 @@
   let
     val _ = Local_Theory.assert_bottom true lthy;
     val target = Named_Target.the_name lthy;
-    val subscribe = if target = "" then Local_Theory.add_registration
-      else Local_Theory.add_dependency target;
+    val subscribe = if target = "" then Generic_Target.theory_registration
+      else Generic_Target.locale_dependency target;
   in
     lthy
     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
diff -r b561cdce6c4c -r f5773a46cf05 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun May 26 19:45:54 2013 +0200
@@ -41,6 +41,10 @@
   val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
     local_theory -> local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
+  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
+  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
 end
 
 structure Generic_Target: GENERIC_TARGET =
@@ -271,6 +275,16 @@
     in generic_const same_shape prmode ((b', mx), rhs') end);
 
 
+(* registrations and dependencies *)
+
+val theory_registration =
+  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
+
+fun locale_dependency locale dep_morph mixin export =
+  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+  #> Local_Theory.activate_nonbrittle dep_morph mixin export;
+
+
 
 (** primitive theory operations **)
 
diff -r b561cdce6c4c -r f5773a46cf05 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun May 26 19:45:54 2013 +0200
@@ -58,9 +58,7 @@
   val const_alias: binding -> string -> local_theory -> local_theory
   val activate: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
-  val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+  val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
@@ -308,19 +306,13 @@
 
 (* activation of locale fragments *)
 
-fun activate_surface dep_morph mixin export =
+fun activate_nonbrittle dep_morph mixin export =
   map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
     (naming, operations, after_close, brittle,
       (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
 
 fun activate dep_morph mixin export =
-  mark_brittle #> activate_surface dep_morph mixin export;
-
-val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
-
-fun add_dependency locale dep_morph mixin export =
-  (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
-  #> activate_surface dep_morph mixin export;
+  mark_brittle #> activate_nonbrittle dep_morph mixin export;
 
 
 (** init and exit **)