# HG changeset patch
# User wenzelm
# Date 883402280 -3600
# Node ID a088ec3e4f5e067fae51eb28069e90e6f86c2737
# Parent  2ba0730672c940c9c3a089d5a257de4fdd55aae5
pretty_name_space;

diff -r 2ba0730672c9 -r a088ec3e4f5e src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Dec 29 14:30:38 1997 +0100
+++ b/src/Pure/display.ML	Mon Dec 29 14:31:20 1997 +0100
@@ -19,6 +19,7 @@
   val print_ctyp	: ctyp -> unit
   val show_consts	: bool ref
   val print_goals	: int -> thm -> unit
+  val pretty_name_space : string * NameSpace.T -> Pretty.T
   val print_syntax	: theory -> unit
   val print_theory	: theory -> unit
   val print_data	: theory -> string -> unit
@@ -107,6 +108,20 @@
 val print_data = Sign.print_data o sign_of;
 
 
+(* pretty_name_space  *)
+
+fun pretty_name_space (kind, space) =
+  let
+    fun prt_entry (name, accs) = Pretty.block
+      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
+        Pretty.commas (map (Pretty.str o quote) accs));
+  in
+    Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
+    |> Pretty.block
+  end;
+
+
+
 (* print signature *)
 
 fun print_sign sg =
@@ -121,9 +136,6 @@
     val ext_const = Sign.cond_extern sg Sign.constK;
 
 
-    fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
-      (map Pretty.str (kind ^ ":" :: map quote (NameSpace.dest space))));
-
     fun pretty_classes cs = Pretty.block
       (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
 
@@ -155,7 +167,7 @@
     Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
     Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
     Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
-    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
+    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
     Pretty.writeln (pretty_classes classes);
     Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
     Pretty.writeln (pretty_default default);
diff -r 2ba0730672c9 -r a088ec3e4f5e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Dec 29 14:30:38 1997 +0100
+++ b/src/Pure/pure_thy.ML	Mon Dec 29 14:31:20 1997 +0100
@@ -63,7 +63,7 @@
       if ! long_names then name else NameSpace.extern space name;
     val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
   in
-    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
+    Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
     Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
   end;