# HG changeset patch
# User haftmann
# Date 1247205569 -7200
# Node ID 801aabf9f376710511051d36217ce7cde7c20af0
# Parent  f4c7be4d684ff7292c74c40c10930b13de3a5b06
tuned locale interface

diff -r f4c7be4d684f -r 801aabf9f376 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:28 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:29 2009 +0200
@@ -242,16 +242,15 @@
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
+    val deps_witss = case some_dep_morph
+     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
+      | NONE => []
   in
     thy
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
-    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
-        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
-          (the_list some_dep_morph)
-    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
-        (Locale.get_registrations thy) thy)
+    |> Locale.add_dependencies sub deps_witss export
   end;
 
 
diff -r f4c7be4d684f -r 801aabf9f376 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:28 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:29 2009 +0200
@@ -796,14 +796,9 @@
   let
     val target = intern thy raw_target;
     val target_ctxt = Locale.init target thy;
-
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-
     fun after_qed witss = ProofContext.theory
-      (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
-        (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
-      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
-        (Locale.get_registrations thy) thy));
+      (Locale.add_dependencies target (deps ~~ witss) export);
   in Element.witness_proof after_qed propss goal_ctxt end;
 
 in
@@ -860,7 +855,7 @@
           end;
 
     fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
-        #-> (fn regs => store_eqns_activate regs eqs));
+      #-> (fn regs => store_eqns_activate regs eqs));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
diff -r f4c7be4d684f -r 801aabf9f376 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:28 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:29 2009 +0200
@@ -45,7 +45,6 @@
   val instance_of: theory -> string -> morphism -> term list
   val specification_of: theory -> string -> term option * term list
   val declarations_of: theory -> string -> declaration list * declaration list
-  val dependencies_of: theory -> string -> (string * morphism) list
 
   (* Storing results *)
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -53,7 +52,6 @@
   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
-  val add_dependency: string -> string * morphism -> theory -> theory
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -69,10 +67,11 @@
   val unfold_add: attribute
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
-  (* Registrations *)
+  (* Registrations and dependencies *)
   val add_registration: string * (morphism * morphism) -> theory -> theory
   val amend_registration: morphism -> string * morphism -> theory -> theory
-  val get_registrations: theory -> (string * morphism) list
+  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
+    morphism  -> theory -> theory
 
   (* Diagnostic *)
   val print_locales: theory -> unit
@@ -338,13 +337,19 @@
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-val get_registrations =
-  Registrations.get #> map (#1 #> apsnd op $>);
+fun reg_morph ((name, (base, export)), _) = (name, base $> export);
+
+fun these_registrations thy name = Registrations.get thy
+  |> filter (curry (op =) name o fst o fst)
+  |> map reg_morph;
+
+fun all_registrations thy = Registrations.get thy
+  |> map reg_morph;
 
 fun add_registration (name, (base_morph, export)) thy =
   roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
-    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
-    (* FIXME |-> put_global_idents ?*)
+    (name, base_morph) (get_idents (Context.Theory thy), thy)
+  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
 
 fun amend_registration morph (name, base_morph) thy =
   let
@@ -364,6 +369,17 @@
   end;
 
 
+(*** Dependencies ***)
+
+fun add_dependencies loc deps_witss export thy =
+  thy
+  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
+      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
+        deps_witss
+  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
+      (all_registrations thy) thy);
+
+
 (*** Storing results ***)
 
 (* Theorems *)
@@ -375,12 +391,12 @@
       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
         #>
       (* Registrations *)
-      (fn thy => fold_rev (fn (name, morph) =>
+      (fn thy => fold_rev (fn (_, morph) =>
             let
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in PureThy.note_thmss kind args'' #> snd end)
-        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+        (these_registrations thy loc) thy))
   in ctxt'' end;
 
 
@@ -404,11 +420,6 @@
 end;
 
 
-(* Dependencies *)
-
-fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
-
-
 (*** Reasoning about locales ***)
 
 (* Storage for witnesses, intro and unfold rules *)