src/Pure/Isar/locale.ML
changeset 36091 055934ed89b0
parent 36090 87e950efb359
child 36093 0880493627ca
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Feb 02 21:23:20 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Feb 11 21:00:36 2010 +0100
     1.3 @@ -349,20 +349,6 @@
     1.4  
     1.5  (* Primitive operations *)
     1.6  
     1.7 -fun compose_mixins mixins =
     1.8 -  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
     1.9 -
    1.10 -fun reg_morph mixins ((name, (base, export)), serial) =
    1.11 -  let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
    1.12 -  in (name, base $> mix $> export) end;
    1.13 -
    1.14 -fun these_registrations thy name = Registrations.get thy
    1.15 -  |>> filter (curry (op =) name o fst o fst)
    1.16 -  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.17 -
    1.18 -fun all_registrations thy = Registrations.get thy
    1.19 -  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.20 -
    1.21  fun get_mixins thy (name, morph) =
    1.22    let
    1.23      val (regs, mixins) = Registrations.get thy;
    1.24 @@ -378,6 +364,22 @@
    1.25      merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
    1.26    |> snd |> filter (snd o fst);  (* only inheritable mixins *)
    1.27  
    1.28 +fun compose_mixins mixins =
    1.29 +  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    1.30 +
    1.31 +fun reg_morph mixins ((name, (base, export)), serial) =
    1.32 +  let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
    1.33 +  in (name, base $> mix $> export) end;
    1.34 +
    1.35 +fun these_registrations thy name = Registrations.get thy
    1.36 +  |>> filter (curry (op =) name o fst o fst)
    1.37 +(*  |-> (fn regs => fn mixins => map (reg_morph mixins) regs); *)
    1.38 +  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
    1.39 +    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.40 +
    1.41 +fun all_registrations thy = Registrations.get thy
    1.42 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.43 +
    1.44  fun activate_notes' activ_elem transfer thy export (name, morph) input =
    1.45    let
    1.46      val {notes, ...} = the_locale thy name;
    1.47 @@ -463,7 +465,8 @@
    1.48        let
    1.49          fun add_reg (dep', morph') =
    1.50            let
    1.51 -            val mixins = collect_mixins thy (dep', morph' $> export);
    1.52 +(*            val mixins = collect_mixins thy (dep', morph' $> export); *)
    1.53 +            val mixins = [];  (* FIXME *)
    1.54              val serial = serial ();
    1.55            in
    1.56              Registrations.map (apfst (cons ((dep', (morph', export)), serial))
    1.57 @@ -510,6 +513,7 @@
    1.58                  Attrib.map_facts (Attrib.attribute_i thy)
    1.59              in PureThy.note_thmss kind args'' #> snd end)
    1.60          (these_registrations thy loc) thy))
    1.61 +(* FIXME apply mixins *)
    1.62    in ctxt'' end;
    1.63  
    1.64