subscription as target-specific implementation device
authorhaftmann
Fri Apr 25 21:45:04 2014 +0200 (2014-04-25)
changeset 56723a8f71445c265
parent 56722 ba1ac087b3a7
child 56724 faa9c21977d2
subscription as target-specific implementation device
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/overloading.ML
src/Tools/permanent_interpretation.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Apr 25 17:54:54 2014 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Apr 25 21:45:04 2014 +0200
     1.3 @@ -585,6 +585,7 @@
     1.4          notes = Generic_Target.notes Generic_Target.theory_notes,
     1.5          abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
     1.6          declaration = K Generic_Target.theory_declaration,
     1.7 +        subscription = Generic_Target.theory_registration,
     1.8          pretty = pretty,
     1.9          exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
    1.10    end;
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Apr 25 17:54:54 2014 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Fri Apr 25 21:45:04 2014 +0200
     2.3 @@ -921,14 +921,9 @@
     2.4  
     2.5  (* second dimension: relation to underlying target *)
     2.6  
     2.7 -fun subscribe lthy =
     2.8 -  if Named_Target.is_theory lthy
     2.9 -  then Generic_Target.theory_registration
    2.10 -  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    2.11 -
    2.12  fun subscribe_or_activate lthy =
    2.13    if Named_Target.is_theory lthy
    2.14 -  then subscribe lthy
    2.15 +  then Local_Theory.subscription
    2.16    else Local_Theory.activate;
    2.17  
    2.18  fun subscribe_locale_only lthy =
    2.19 @@ -937,7 +932,7 @@
    2.20        if Named_Target.is_theory lthy
    2.21        then error "Not possible on level of global theory"
    2.22        else ();
    2.23 -  in subscribe lthy end;
    2.24 +  in Local_Theory.subscription end;
    2.25  
    2.26  
    2.27  (* special case: global sublocale command *)
    2.28 @@ -964,7 +959,7 @@
    2.29  fun interpret_cmd x = gen_interpret read_interpretation x;
    2.30  
    2.31  fun permanent_interpretation x =
    2.32 -  gen_local_theory_interpretation cert_interpretation subscribe x;
    2.33 +  gen_local_theory_interpretation cert_interpretation (K Local_Theory.subscription) x;
    2.34  
    2.35  fun ephemeral_interpretation x =
    2.36    gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
     3.1 --- a/src/Pure/Isar/local_theory.ML	Fri Apr 25 17:54:54 2014 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Apr 25 21:45:04 2014 +0200
     3.3 @@ -49,6 +49,8 @@
     3.4    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     3.5      (term * term) * local_theory
     3.6    val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
     3.7 +  val subscription: string * morphism -> (morphism * bool) option -> morphism ->
     3.8 +    local_theory -> local_theory
     3.9    val pretty: local_theory -> Pretty.T list
    3.10    val set_defsort: sort -> local_theory -> local_theory
    3.11    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    3.12 @@ -83,6 +85,8 @@
    3.13    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    3.14      (term * term) * local_theory,
    3.15    declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
    3.16 +  subscription: string * morphism -> (morphism * bool) option -> morphism ->
    3.17 +     local_theory -> local_theory,
    3.18    pretty: local_theory -> Pretty.T list,
    3.19    exit: local_theory -> Proof.context};
    3.20  
    3.21 @@ -252,6 +256,7 @@
    3.22  
    3.23  fun operation f lthy = f (operations_of lthy) lthy;
    3.24  fun operation2 f x y = operation (fn ops => f ops x y);
    3.25 +fun operation3 f x y z = operation (fn ops => f ops x y z);
    3.26  
    3.27  val pretty = operation #pretty;
    3.28  val abbrev = operation2 #abbrev;
    3.29 @@ -259,6 +264,7 @@
    3.30  val define_internal = operation2 #define true;
    3.31  val notes_kind = operation2 #notes;
    3.32  val declaration = operation2 #declaration;
    3.33 +val subscription = operation3 #subscription;
    3.34  
    3.35  
    3.36  (* basic derived operations *)
     4.1 --- a/src/Pure/Isar/named_target.ML	Fri Apr 25 17:54:54 2014 +0200
     4.2 +++ b/src/Pure/Isar/named_target.ML	Fri Apr 25 21:45:04 2014 +0200
     4.3 @@ -134,6 +134,14 @@
     4.4      |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
     4.5  
     4.6  
     4.7 +(* subscription *)
     4.8 +
     4.9 +fun target_subscription (Target {target, ...}) =
    4.10 +  if target = ""
    4.11 +  then Generic_Target.theory_registration
    4.12 +  else Generic_Target.locale_dependency target
    4.13 +
    4.14 +
    4.15  (* pretty *)
    4.16  
    4.17  fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
    4.18 @@ -183,6 +191,7 @@
    4.19          notes = Generic_Target.notes (target_notes ta),
    4.20          abbrev = Generic_Target.abbrev (target_abbrev ta),
    4.21          declaration = target_declaration ta,
    4.22 +        subscription = target_subscription ta,
    4.23          pretty = pretty ta,
    4.24          exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
    4.25    end;
     5.1 --- a/src/Pure/Isar/overloading.ML	Fri Apr 25 17:54:54 2014 +0200
     5.2 +++ b/src/Pure/Isar/overloading.ML	Fri Apr 25 21:45:04 2014 +0200
     5.3 @@ -205,6 +205,7 @@
     5.4          notes = Generic_Target.notes Generic_Target.theory_notes,
     5.5          abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
     5.6          declaration = K Generic_Target.theory_declaration,
     5.7 +        subscription = Generic_Target.theory_registration,
     5.8          pretty = pretty,
     5.9          exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
    5.10    end;
     6.1 --- a/src/Tools/permanent_interpretation.ML	Fri Apr 25 17:54:54 2014 +0200
     6.2 +++ b/src/Tools/permanent_interpretation.ML	Fri Apr 25 21:45:04 2014 +0200
     6.3 @@ -85,13 +85,8 @@
     6.4  
     6.5  (* interpretation with permanent registration *)
     6.6  
     6.7 -fun subscribe lthy =
     6.8 -  if Named_Target.is_theory lthy
     6.9 -  then Generic_Target.theory_registration
    6.10 -  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    6.11 -
    6.12  fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
    6.13 -  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
    6.14 +  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.subscription
    6.15      expression raw_defs raw_eqns lthy
    6.16  
    6.17  in