src/Pure/Isar/locale.ML
changeset 69056 bc4cc763b0ea
parent 69055 dab89758545c
child 69057 56c6378ebaea
equal deleted inserted replaced
69055:dab89758545c 69056:bc4cc763b0ea
   418     |> snd |> filter (snd o fst)  (* only inheritable mixins *)
   418     |> snd |> filter (snd o fst)  (* only inheritable mixins *)
   419     |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
   419     |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
   420     |> compose_mixins
   420     |> compose_mixins
   421   end;
   421   end;
   422 
   422 
   423 fun registrations_of context loc =
       
   424   Idtab.fold_rev (fn ((name, _), {morphisms, ...}) =>
       
   425     name = loc ? cons (name, morphisms)) (get_regs context) []
       
   426   (* with inherited mixins *)
       
   427   |> map (fn (name, (base, export)) =>
       
   428       (name, base $> (collect_mixins context (name, base $> export)) $> export));
       
   429 
       
   430 
   423 
   431 (*** Activate context elements of locale ***)
   424 (*** Activate context elements of locale ***)
   432 
   425 
   433 fun activate_err msg (name, morph) context =
   426 fun activate_err msg (name, morph) context =
   434   cat_error msg ("The above error(s) occurred while activating locale instance\n" ^
   427   cat_error msg ("The above error(s) occurred while activating locale instance\n" ^
   603 
   596 
   604 
   597 
   605 
   598 
   606 (*** Dependencies ***)
   599 (*** Dependencies ***)
   607 
   600 
       
   601 fun registrations_of context loc =
       
   602   Idtab.fold_rev (fn ((name, _), {morphisms, ...}) =>
       
   603     name = loc ? cons (name, morphisms)) (get_regs context) []
       
   604   (*with inherited mixins*)
       
   605   |> map (fn (name, (base, export)) =>
       
   606       (name, base $> (collect_mixins context (name, base $> export)) $> export));
       
   607 
   608 fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   608 fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   609   let
   609   let
   610     val serial' = serial ();
   610     val serial' = serial ();
   611     val thy' = thy |>
   611     val thy' = thy |>
   612       (change_locale loc o apsnd)
   612       (change_locale loc o apsnd)