equal
deleted
inserted
replaced
107 lists indexed by registration/dependency serial, |
107 lists indexed by registration/dependency serial, |
108 entries for empty lists may be omitted*) |
108 entries for empty lists may be omitted*) |
109 type mixin = (morphism * bool) * serial; |
109 type mixin = (morphism * bool) * serial; |
110 type mixins = mixin list Inttab.table; |
110 type mixins = mixin list Inttab.table; |
111 |
111 |
112 fun lookup_mixins serial' (mixins: mixins) = Inttab.lookup_list mixins serial'; |
112 fun lookup_mixins (mixins: mixins) serial' = Inttab.lookup_list mixins serial'; |
113 |
113 |
114 val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); |
114 val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); |
115 |
115 |
116 fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); |
116 fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); |
117 |
117 |
226 |
226 |
227 fun hyp_spec_of thy = #hyp_spec o the_locale thy; |
227 fun hyp_spec_of thy = #hyp_spec o the_locale thy; |
228 |
228 |
229 fun dependencies_of thy = #dependencies o the_locale thy; |
229 fun dependencies_of thy = #dependencies o the_locale thy; |
230 |
230 |
231 fun mixins_of thy name serial = the_locale thy name |> |
231 fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; |
232 #mixins |> lookup_mixins serial; |
|
233 |
232 |
234 (* FIXME unused!? *) |
233 (* FIXME unused!? *) |
235 fun identity_on thy name morph = |
234 fun identity_on thy name morph = |
236 let val mk_instance = instance_of thy name |
235 let val mk_instance = instance_of thy name |
237 in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end; |
236 in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end; |
381 val thy = Context.theory_of context; |
380 val thy = Context.theory_of context; |
382 val (regs, mixins) = Registrations.get context; |
381 val (regs, mixins) = Registrations.get context; |
383 in |
382 in |
384 (case Idtab.lookup regs (name, instance_of thy name morph) of |
383 (case Idtab.lookup regs (name, instance_of thy name morph) of |
385 NONE => [] |
384 NONE => [] |
386 | SOME (_, serial) => lookup_mixins serial mixins) |
385 | SOME (_, serial) => lookup_mixins mixins serial) |
387 end; |
386 end; |
388 |
387 |
389 fun collect_mixins context (name, morph) = |
388 fun collect_mixins context (name, morph) = |
390 let |
389 let |
391 val thy = Context.theory_of context; |
390 val thy = Context.theory_of context; |