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