src/Pure/Isar/locale.ML

--- a/src/Pure/Isar/locale.ML	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 26 14:23:33 2012 +0200
@@ -76,14 +76,11 @@
     morphism -> theory -> theory
 
   (* Diagnostic *)
-  val all_locales: theory -> string list
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> 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
+  val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
 end;
 
 structure Locale: LOCALE =
@@ -610,16 +607,13 @@
 
 (*** diagnostic commands and interfaces ***)
 
-val all_locales = Symtab.keys o snd o Locales.get;
-
 fun print_locales thy =
   Pretty.strs ("locales:" ::
     map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
   |> Pretty.writeln;
 
-fun print_locale thy show_facts raw_name =
+fun pretty_locale thy show_facts name =
   let
-    val name = check thy raw_name;
     val ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
@@ -627,10 +621,14 @@
       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
-    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
-    |> Pretty.writeln
+    Pretty.block
+      (Pretty.command "locale" :: Pretty.brk 1 :: Pretty.str (extern thy name) ::
+        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt ctxt elem)]) elems)
   end;
 
+fun print_locale thy show_facts raw_name =
+  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+
 fun print_registrations ctxt raw_name =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -651,34 +649,12 @@
     | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
   end |> Pretty.writeln;
 
-fun locale_deps thy =
+fun pretty_locale_deps thy =
   let
-    val names = all_locales thy;
-    fun add_locale_node name =
-      let
-        val params = params_of thy name;
-        val axioms =
-          these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
-        val registrations =
-          map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
-      in
-        Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
-      end;
-    fun add_locale_deps name =
-      let
-        val dependencies =
-          map (apsnd (instance_of thy name o op $>) o fst) (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;
+    fun make_node name =
+     {name = name,
+      parents = map (fst o fst) (dependencies_of thy name),
+      body = pretty_locale thy false name};
+  in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
 
 end;