Explicitly manage export in dependencies.
authorballarin
Tue Apr 27 22:27:22 2010 +0200 (2010-04-27)
changeset 3665197c3bbe63389
parent 36338 7808fbc9c3b4
child 36652 aace7a969410
Explicitly manage export in dependencies.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Sat Apr 24 21:29:22 2010 -0700
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Apr 27 22:27:22 2010 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4      (* syntax declarations *)
     1.5    notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
     1.6      (* theorem declarations *)
     1.7 -  dependencies: ((string * morphism) * serial) list
     1.8 +  dependencies: ((string * (morphism * morphism)) * serial) list
     1.9      (* locale dependencies (sublocale relation) *)
    1.10  };
    1.11  
    1.12 @@ -143,7 +143,8 @@
    1.13      (binding,
    1.14        mk_locale ((parameters, spec, intros, axioms),
    1.15          ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
    1.16 -          map (fn d => (d, serial ())) dependencies))) #> snd);
    1.17 +          map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
    1.18 +          (* FIXME *)
    1.19  
    1.20  fun change_locale name =
    1.21    Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    1.22 @@ -223,7 +224,7 @@
    1.23        then (deps, marked)
    1.24        else
    1.25          let
    1.26 -          val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
    1.27 +          val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
    1.28            val marked' = (name, instance) :: marked;
    1.29            val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
    1.30          in
    1.31 @@ -489,7 +490,7 @@
    1.32  
    1.33  fun add_dependency loc (dep, morph) export thy =
    1.34    thy
    1.35 -  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
    1.36 +  |> (change_locale loc o apsnd) (cons ((dep, (morph, export)), serial ()))
    1.37    |> (fn thy => fold_rev (add_reg_activate_facts export)
    1.38        (all_registrations thy) thy);
    1.39