more specific structure for registration into theory and dependency onto locale
authorhaftmann
Sun May 26 19:45:54 2013 +0200 (2013-05-26)
changeset 52153f5773a46cf05
parent 52152 b561cdce6c4c
child 52164 3c18725d576a
more specific structure for registration into theory and dependency onto locale
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun May 26 19:45:54 2013 +0200
     1.3 @@ -882,7 +882,7 @@
     1.4    then 
     1.5      lthy
     1.6      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
     1.7 -        Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
     1.8 +        Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
     1.9    else
    1.10      lthy
    1.11      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.12 @@ -895,7 +895,7 @@
    1.13    in
    1.14      lthy
    1.15      |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.16 -        Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
    1.17 +        Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
    1.18    end;
    1.19    
    1.20  fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    1.21 @@ -915,8 +915,8 @@
    1.22    let
    1.23      val _ = Local_Theory.assert_bottom true lthy;
    1.24      val target = Named_Target.the_name lthy;
    1.25 -    val subscribe = if target = "" then Local_Theory.add_registration
    1.26 -      else Local_Theory.add_dependency target;
    1.27 +    val subscribe = if target = "" then Generic_Target.theory_registration
    1.28 +      else Generic_Target.locale_dependency target;
    1.29    in
    1.30      lthy
    1.31      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
     2.1 --- a/src/Pure/Isar/generic_target.ML	Sun May 26 19:45:54 2013 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Sun May 26 19:45:54 2013 +0200
     2.3 @@ -41,6 +41,10 @@
     2.4    val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
     2.5      local_theory -> local_theory
     2.6    val theory_declaration: declaration -> local_theory -> local_theory
     2.7 +  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     2.8 +    local_theory -> local_theory
     2.9 +  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
    2.10 +    local_theory -> local_theory
    2.11  end
    2.12  
    2.13  structure Generic_Target: GENERIC_TARGET =
    2.14 @@ -271,6 +275,16 @@
    2.15      in generic_const same_shape prmode ((b', mx), rhs') end);
    2.16  
    2.17  
    2.18 +(* registrations and dependencies *)
    2.19 +
    2.20 +val theory_registration =
    2.21 +  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    2.22 +
    2.23 +fun locale_dependency locale dep_morph mixin export =
    2.24 +  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    2.25 +  #> Local_Theory.activate_nonbrittle dep_morph mixin export;
    2.26 +
    2.27 +
    2.28  
    2.29  (** primitive theory operations **)
    2.30  
     3.1 --- a/src/Pure/Isar/local_theory.ML	Sun May 26 19:45:54 2013 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sun May 26 19:45:54 2013 +0200
     3.3 @@ -58,9 +58,7 @@
     3.4    val const_alias: binding -> string -> local_theory -> local_theory
     3.5    val activate: string * morphism -> (morphism * bool) option -> morphism ->
     3.6      local_theory -> local_theory
     3.7 -  val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
     3.8 -    local_theory -> local_theory
     3.9 -  val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
    3.10 +  val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    3.11      local_theory -> local_theory
    3.12    val init: Name_Space.naming -> operations -> Proof.context -> local_theory
    3.13    val exit: local_theory -> Proof.context
    3.14 @@ -308,19 +306,13 @@
    3.15  
    3.16  (* activation of locale fragments *)
    3.17  
    3.18 -fun activate_surface dep_morph mixin export =
    3.19 +fun activate_nonbrittle dep_morph mixin export =
    3.20    map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
    3.21      (naming, operations, after_close, brittle,
    3.22        (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
    3.23  
    3.24  fun activate dep_morph mixin export =
    3.25 -  mark_brittle #> activate_surface dep_morph mixin export;
    3.26 -
    3.27 -val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
    3.28 -
    3.29 -fun add_dependency locale dep_morph mixin export =
    3.30 -  (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    3.31 -  #> activate_surface dep_morph mixin export;
    3.32 +  mark_brittle #> activate_nonbrittle dep_morph mixin export;
    3.33  
    3.34  
    3.35  (** init and exit **)