Cleaner implementation of sublocale command.
authorballarin
Mon May 24 10:48:32 2010 +0200 (2010-05-24)
changeset 37102785348a83a2b
parent 37101 7099a9ed3be2
child 37103 6ea25bb157e1
Cleaner implementation of sublocale command.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.3 @@ -368,7 +368,7 @@
     1.4  fun collect_mixins thy (name, morph) =
     1.5    roundup thy (fn dep => fn mixins =>
     1.6      merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
     1.7 -  |> snd |> filter (snd o fst);  (* only inheritable mixins *)
     1.8 +  |> snd |> filter (snd o fst);  (* only inheritable mixins *) (* FIXME *)
     1.9    (* FIXME refactor usage *)
    1.10  
    1.11  fun compose_mixins mixins =
    1.12 @@ -462,38 +462,37 @@
    1.13  
    1.14  fun add_registration (name, base_morph) mixin export thy =
    1.15    let
    1.16 -    val base = instance_of thy name base_morph;
    1.17      val mix = case mixin of NONE => Morphism.identity
    1.18            | SOME (mix, _) => mix;
    1.19 +    val morph = base_morph $> mix;
    1.20 +    val inst = instance_of thy name morph;
    1.21    in
    1.22 -    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
    1.23 +    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, inst)
    1.24      then thy
    1.25      else
    1.26        (get_idents (Context.Theory thy), thy)
    1.27        (* add new registrations with inherited mixins *)
    1.28 -      |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
    1.29 +      |> roundup thy (add_reg export) export (name, morph)
    1.30        |> snd
    1.31        (* add mixin *)
    1.32        |> (case mixin of NONE => I
    1.33 -           | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
    1.34 +           | SOME mixin => amend_registration (name, morph) mixin export)
    1.35        (* activate import hierarchy as far as not already active *)
    1.36 -      |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
    1.37 +      |> Context.theory_map (activate_facts' export (name, morph))
    1.38    end;
    1.39  
    1.40  
    1.41  (*** Dependencies ***)
    1.42  
    1.43 -fun add_reg_activate_facts export (dep, morph) thy =
    1.44 -  (get_idents (Context.Theory thy), thy)
    1.45 -  |> roundup thy (add_reg export) export (dep, morph)
    1.46 -  |> snd
    1.47 -  |> Context.theory_map (activate_facts' export (dep, morph));
    1.48 -
    1.49 -fun add_dependency loc (dep, morph) export thy =
    1.50 -  thy
    1.51 -  |> (change_locale loc o apsnd) (cons ((dep, (morph, export)), serial ()))
    1.52 -  |> (fn thy => fold_rev (add_reg_activate_facts export)
    1.53 -      (all_registrations thy) thy);
    1.54 +fun add_dependency loc (name, morph) export thy =
    1.55 +  let
    1.56 +    val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
    1.57 +    val (_, regs) = fold_rev (roundup thy' cons export)
    1.58 +      (all_registrations thy') (get_idents (Context.Theory thy'), []);
    1.59 +  in
    1.60 +    thy'
    1.61 +    |> fold_rev (fn dep => add_registration dep NONE export) regs
    1.62 +  end;
    1.63  
    1.64  
    1.65  (*** Storing results ***)