# HG changeset patch # User ballarin # Date 1277228776 -7200 # Node ID b5989aa323582bda264a081cd8c503611ef1ddfb # Parent 9de1add14bac1fb496481415608be53935f3b833 Proper treatment of non-inherited mixins. diff -r 9de1add14bac -r b5989aa32358 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/Pure/Isar/locale.ML Tue Jun 22 19:46:16 2010 +0200 @@ -396,38 +396,33 @@ | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial) end; -fun collect_mixins thy (name, morph) = - roundup thy (fn dep => fn mixins => - merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], []) - |> snd |> filter (snd o fst); (* only inheritable mixins *) (* FIXME *) - (* FIXME refactor usage *) - fun compose_mixins mixins = fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; -fun reg_morph mixins ((name, (base, export)), serial) = - let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins; - in (name, base $> mix $> export) end; +fun collect_mixins thy (name, morph) = + roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins thy dep)) + Morphism.identity (name, morph) ([(name, instance_of thy name morph)], []) + |> snd |> filter (snd o fst) (* only inheritable mixins *) + |> (fn x => merge (eq_snd op =) (x, get_mixins thy (name, morph))) + |> compose_mixins; -fun these_registrations thy name = Registrations.get thy - |>> Idtab.dest - |>> filter (curry (op =) name o fst o fst) +fun get_registrations thy select = Registrations.get thy + |>> Idtab.dest |>> select (* with inherited mixins *) |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) => - (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs); + (name, base $> (collect_mixins thy (name, base $> export)) $> export)) regs); -fun all_registrations thy = Registrations.get thy (* FIXME clone *) - |>> Idtab.dest - (* with inherited mixins *) - |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) => - (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs); +fun these_registrations thy name = + get_registrations thy (filter (curry (op =) name o fst o fst)); + +fun all_registrations thy = get_registrations thy I; fun activate_notes' activ_elem transfer thy export (name, morph) input = let val {notes, ...} = the_locale thy name; fun activate ((kind, facts), _) input = let - val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins; + val mixin = collect_mixins thy (name, morph $> export); val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export)) in activ_elem (Notes (kind, facts')) input end; in