load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
authorwenzelm
Wed Aug 13 13:30:28 2014 +0200 (2014-08-13)
changeset 5792659b2572e8e93
parent 57925 2bd92d3f92d7
child 57927 f14c1248d064
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Aug 13 12:59:27 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Aug 13 13:30:28 2014 +0200
     1.3 @@ -924,7 +924,7 @@
     1.4  fun subscribe_or_activate lthy =
     1.5    if Named_Target.is_theory lthy
     1.6    then Local_Theory.subscription
     1.7 -  else Local_Theory.activate;
     1.8 +  else Locale.activate_fragment;
     1.9  
    1.10  fun subscribe_locale_only lthy =
    1.11    let
    1.12 @@ -964,7 +964,7 @@
    1.13      (K Local_Theory.subscription) expression raw_eqns;
    1.14  
    1.15  fun ephemeral_interpretation x =
    1.16 -  gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
    1.17 +  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
    1.18  
    1.19  fun interpretation x =
    1.20    gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
     2.1 --- a/src/Pure/Isar/generic_target.ML	Wed Aug 13 12:59:27 2014 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Aug 13 13:30:28 2014 +0200
     2.3 @@ -358,6 +358,6 @@
     2.4  
     2.5  fun locale_dependency locale dep_morph mixin export =
     2.6    (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
     2.7 -  #> Local_Theory.activate_nonbrittle dep_morph mixin export;
     2.8 +  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
     2.9  
    2.10  end;
     3.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:59:27 2014 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 13:30:28 2014 +0200
     3.3 @@ -7,6 +7,12 @@
     3.4  type local_theory = Proof.context;
     3.5  type generic_theory = Context.generic;
     3.6  
     3.7 +structure Attrib =
     3.8 +struct
     3.9 +  type src = Args.src;
    3.10 +  type binding = binding * src list;
    3.11 +end;
    3.12 +
    3.13  signature LOCAL_THEORY =
    3.14  sig
    3.15    type operations
    3.16 @@ -14,6 +20,7 @@
    3.17    val restore: local_theory -> local_theory
    3.18    val level: Proof.context -> int
    3.19    val assert_bottom: bool -> local_theory -> local_theory
    3.20 +  val mark_brittle: local_theory -> local_theory
    3.21    val assert_nonbrittle: local_theory -> local_theory
    3.22    val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
    3.23      local_theory -> local_theory
    3.24 @@ -58,10 +65,6 @@
    3.25    val class_alias: binding -> class -> local_theory -> local_theory
    3.26    val type_alias: binding -> string -> local_theory -> local_theory
    3.27    val const_alias: binding -> string -> local_theory -> local_theory
    3.28 -  val activate: string * morphism -> (morphism * bool) option -> morphism ->
    3.29 -    local_theory -> local_theory
    3.30 -  val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    3.31 -    local_theory -> local_theory
    3.32    val init: Name_Space.naming -> operations -> Proof.context -> local_theory
    3.33    val exit: local_theory -> Proof.context
    3.34    val exit_global: local_theory -> theory
    3.35 @@ -307,17 +310,6 @@
    3.36  val const_alias = alias Sign.const_alias Proof_Context.const_alias;
    3.37  
    3.38  
    3.39 -(* activation of locale fragments *)
    3.40 -
    3.41 -fun activate_nonbrittle dep_morph mixin export =
    3.42 -  map_top (fn (naming, operations, after_close, brittle, target) =>
    3.43 -    (naming, operations, after_close, brittle,
    3.44 -      (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
    3.45 -
    3.46 -fun activate dep_morph mixin export =
    3.47 -  mark_brittle #> activate_nonbrittle dep_morph mixin export;
    3.48 -
    3.49 -
    3.50  
    3.51  (** init and exit **)
    3.52  
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 13 12:59:27 2014 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 13 13:30:28 2014 +0200
     4.3 @@ -70,6 +70,10 @@
     4.4    (* Registrations and dependencies *)
     4.5    val add_registration: string * morphism -> (morphism * bool) option ->
     4.6      morphism -> Context.generic -> Context.generic
     4.7 +  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
     4.8 +    local_theory -> local_theory
     4.9 +  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    4.10 +    local_theory -> local_theory
    4.11    val amend_registration: string * morphism -> morphism * bool ->
    4.12      morphism -> Context.generic -> Context.generic
    4.13    val registrations_of: Context.generic -> string -> (string * morphism) list
    4.14 @@ -514,6 +518,19 @@
    4.15    end;
    4.16  
    4.17  
    4.18 +(* locale fragments within local theory *)
    4.19 +
    4.20 +fun activate_fragment_nonbrittle dep_morph mixin export lthy =
    4.21 +  let val n = Local_Theory.level lthy in
    4.22 +    lthy |> Local_Theory.map_contexts (fn level =>
    4.23 +      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
    4.24 +  end;
    4.25 +
    4.26 +fun activate_fragment dep_morph mixin export =
    4.27 +  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
    4.28 +
    4.29 +
    4.30 +
    4.31  (*** Dependencies ***)
    4.32  
    4.33  (* FIXME dead code!?
     5.1 --- a/src/Pure/ROOT.ML	Wed Aug 13 12:59:27 2014 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Wed Aug 13 13:30:28 2014 +0200
     5.3 @@ -234,7 +234,8 @@
     5.4  use "Isar/parse.ML";
     5.5  use "Isar/args.ML";
     5.6  
     5.7 -(*theory sources*)
     5.8 +(*theory specifications*)
     5.9 +use "Isar/local_theory.ML";
    5.10  use "Thy/thy_header.ML";
    5.11  use "PIDE/command_span.ML";
    5.12  use "Thy/thy_syntax.ML";
    5.13 @@ -264,7 +265,6 @@
    5.14  
    5.15  (*local theories and targets*)
    5.16  use "Isar/locale.ML";
    5.17 -use "Isar/local_theory.ML";
    5.18  use "Isar/generic_target.ML";
    5.19  use "Isar/overloading.ML";
    5.20  use "axclass.ML";