# HG changeset patch
# User ballarin
# Date 1272400042 -7200
# Node ID 97c3bbe63389ab5a0c440af1c2a23a668cdd5329
# Parent  7808fbc9c3b4b2f2a44f7cbf5d7f9ad211a63495
Explicitly manage export in dependencies.

diff -r 7808fbc9c3b4 -r 97c3bbe63389 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Apr 24 21:29:22 2010 -0700
+++ b/src/Pure/Isar/locale.ML	Tue Apr 27 22:27:22 2010 +0200
@@ -99,7 +99,7 @@
     (* syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
     (* theorem declarations *)
-  dependencies: ((string * morphism) * serial) list
+  dependencies: ((string * (morphism * morphism)) * serial) list
     (* locale dependencies (sublocale relation) *)
 };
 
@@ -143,7 +143,8 @@
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
-          map (fn d => (d, serial ())) dependencies))) #> snd);
+          map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
+          (* FIXME *)
 
 fun change_locale name =
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -223,7 +224,7 @@
       then (deps, marked)
       else
         let
-          val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
+          val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
           val marked' = (name, instance) :: marked;
           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
         in
@@ -489,7 +490,7 @@
 
 fun add_dependency loc (dep, morph) export thy =
   thy
-  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
+  |> (change_locale loc o apsnd) (cons ((dep, (morph, export)), serial ()))
   |> (fn thy => fold_rev (add_reg_activate_facts export)
       (all_registrations thy) thy);