# 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;