src/Pure/Isar/locale.ML
changeset 32803 fc02b4b9eccc
parent 32800 57fcca4e7c0e
child 32804 ca430e6aee1c
     1.1 --- a/src/Pure/Isar/locale.ML	Sat Sep 26 21:03:57 2009 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sun Sep 27 11:50:27 2009 +0200
     1.3 @@ -212,13 +212,13 @@
     1.4  
     1.5  val roundup_bound = 120;
     1.6  
     1.7 -fun add thy depth (name, morph) (deps, marked) =
     1.8 +fun add thy depth export (name, morph) (deps, marked) =
     1.9    if depth > roundup_bound
    1.10    then error "Roundup bound exceeded (sublocale relation probably not terminating)."
    1.11    else
    1.12      let
    1.13        val dependencies = dependencies_of thy name;
    1.14 -      val instance = instance_of thy name morph;
    1.15 +      val instance = instance_of thy name (morph $> export);
    1.16      in
    1.17        if member (ident_eq thy) marked (name, instance)
    1.18        then (deps, marked)
    1.19 @@ -226,7 +226,7 @@
    1.20          let
    1.21            val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
    1.22            val marked' = (name, instance) :: marked;
    1.23 -          val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
    1.24 +          val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
    1.25          in
    1.26            ((name, morph) :: deps' @ deps, marked'')
    1.27          end
    1.28 @@ -234,14 +234,17 @@
    1.29  
    1.30  in
    1.31  
    1.32 -fun roundup thy activate_dep (name, morph) (marked, input) =
    1.33 +(* Note that while identifiers always have the exported view, activate_dep is
    1.34 +  is presented with the internal view. *)
    1.35 +
    1.36 +fun roundup thy activate_dep export (name, morph) (marked, input) =
    1.37    let
    1.38      (* Find all dependencies incuding new ones (which are dependencies enriching
    1.39        existing registrations). *)
    1.40 -    val (dependencies, marked') = add thy 0 (name, morph) ([], []);
    1.41 +    val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
    1.42      (* Filter out fragments from marked; these won't be activated. *)
    1.43      val dependencies' = filter_out (fn (name, morph) =>
    1.44 -      member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
    1.45 +      member (ident_eq thy) marked (name, instance_of thy name (morph $> export))) dependencies;
    1.46    in
    1.47      (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
    1.48    end;
    1.49 @@ -285,7 +288,7 @@
    1.50          else I);
    1.51      val activate = activate_notes activ_elem transfer thy;
    1.52    in
    1.53 -    roundup thy activate (name, Morphism.identity) (marked, input')
    1.54 +    roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
    1.55    end;
    1.56  
    1.57  
    1.58 @@ -294,13 +297,13 @@
    1.59  fun activate_declarations dep = Context.proof_map (fn context =>
    1.60    let
    1.61      val thy = Context.theory_of context;
    1.62 -  in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
    1.63 +  in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
    1.64  
    1.65  fun activate_facts dep context =
    1.66    let
    1.67      val thy = Context.theory_of context;
    1.68      val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
    1.69 -  in roundup thy activate dep (get_idents context, context) |-> put_idents end;
    1.70 +  in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
    1.71  
    1.72  fun init name thy =
    1.73    activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    1.74 @@ -369,7 +372,7 @@
    1.75    in
    1.76      (get_idents (Context.Theory thy), thy)
    1.77      |> roundup thy (fn (dep', morph') =>
    1.78 -        Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
    1.79 +        Registrations.map (cons ((dep', (morph', export)), stamp ()))) export (dep, morph)
    1.80      |> snd
    1.81      |> Context.theory_map (activate_facts (dep, morph $> export))
    1.82    end;