src/Pure/Isar/locale.ML
changeset 36905 b47fd7148b57
parent 36653 8629ac3efb19
child 36919 182774d56bd2
     1.1 --- a/src/Pure/Isar/locale.ML	Thu May 13 13:29:43 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu May 13 13:30:16 2010 +0200
     1.3 @@ -384,9 +384,10 @@
     1.4    |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
     1.5      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
     1.6  
     1.7 -fun all_registrations thy = Registrations.get thy
     1.8 -  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
     1.9 -  (* without inherited mixins *)
    1.10 +fun all_registrations thy = Registrations.get thy (* FIXME clone *)
    1.11 +  (* with inherited mixins *)
    1.12 +  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
    1.13 +    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.14  
    1.15  fun activate_notes' activ_elem transfer thy export (name, morph) input =
    1.16    let
    1.17 @@ -462,19 +463,21 @@
    1.18  fun add_registration (name, base_morph) mixin export thy =
    1.19    let
    1.20      val base = instance_of thy name base_morph;
    1.21 +    val mix = case mixin of NONE => Morphism.identity
    1.22 +          | SOME (mix, _) => mix;
    1.23    in
    1.24      if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
    1.25      then thy
    1.26      else
    1.27        (get_idents (Context.Theory thy), thy)
    1.28        (* add new registrations with inherited mixins *)
    1.29 -      |> roundup thy (add_reg export) export (name, base_morph)
    1.30 +      |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
    1.31        |> snd
    1.32        (* add mixin *)
    1.33        |> (case mixin of NONE => I
    1.34 -           | SOME mixin => amend_registration (name, base_morph) mixin export)
    1.35 +           | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
    1.36        (* activate import hierarchy as far as not already active *)
    1.37 -      |> Context.theory_map (activate_facts' export (name, base_morph))
    1.38 +      |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
    1.39    end;
    1.40  
    1.41