# HG changeset patch
# User haftmann
# Date 1279698396 -7200
# Node ID c5ad6fec34701501898b945d696d69b27adea498
# Parent  4274a8d60fa134b6fc1c17aed3569c0d15ac79b8
abstract visualization of locale ingredients; all_locales yields proper locale identifiers

diff -r 4274a8d60fa1 -r c5ad6fec3470 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jul 20 14:08:47 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 21 09:46:36 2010 +0200
@@ -77,6 +77,9 @@
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
   val print_registrations: theory -> string -> unit
+  val locale_deps: theory ->
+    { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
+      * term list list Symtab.table Symtab.table
 end;
 
 structure Locale: LOCALE =
@@ -567,10 +570,10 @@
 
 (*** diagnostic commands and interfaces ***)
 
-fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy));
+val all_locales = Symtab.keys o snd o Locales.get;
 
 fun print_locales thy =
-  Pretty.strs ("locales:" :: all_locales thy)
+  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   |> Pretty.writeln;
 
 fun print_locale thy show_facts raw_name =
@@ -593,4 +596,32 @@
     | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   |> Pretty.writeln;
 
+fun locale_deps thy =
+  let
+    val names = all_locales thy
+    fun add_locale_node name =
+      let
+        val params = params_of thy name;
+        val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
+        val registrations = map (instance_of thy name o snd)
+          (these_registrations thy name);
+      in 
+        Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
+      end;
+    fun add_locale_deps name =
+      let
+        val dependencies = (map o apsnd) (instance_of thy name o op $>)
+          (dependencies_of thy name);
+      in
+        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+          deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
+            dependencies
+      end;
+  in
+    Graph.empty
+    |> fold add_locale_node names
+    |> rpair Symtab.empty
+    |> fold add_locale_deps names
+  end;
+
 end;