pretty_name_space;
authorwenzelm
Mon Dec 29 14:31:20 1997 +0100 (1997-12-29)
changeset 4498a088ec3e4f5e
parent 4497 2ba0730672c9
child 4499 4ca67338e22c
pretty_name_space;
src/Pure/display.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/display.ML	Mon Dec 29 14:30:38 1997 +0100
     1.2 +++ b/src/Pure/display.ML	Mon Dec 29 14:31:20 1997 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val print_ctyp	: ctyp -> unit
     1.5    val show_consts	: bool ref
     1.6    val print_goals	: int -> thm -> unit
     1.7 +  val pretty_name_space : string * NameSpace.T -> Pretty.T
     1.8    val print_syntax	: theory -> unit
     1.9    val print_theory	: theory -> unit
    1.10    val print_data	: theory -> string -> unit
    1.11 @@ -107,6 +108,20 @@
    1.12  val print_data = Sign.print_data o sign_of;
    1.13  
    1.14  
    1.15 +(* pretty_name_space  *)
    1.16 +
    1.17 +fun pretty_name_space (kind, space) =
    1.18 +  let
    1.19 +    fun prt_entry (name, accs) = Pretty.block
    1.20 +      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
    1.21 +        Pretty.commas (map (Pretty.str o quote) accs));
    1.22 +  in
    1.23 +    Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
    1.24 +    |> Pretty.block
    1.25 +  end;
    1.26 +
    1.27 +
    1.28 +
    1.29  (* print signature *)
    1.30  
    1.31  fun print_sign sg =
    1.32 @@ -121,9 +136,6 @@
    1.33      val ext_const = Sign.cond_extern sg Sign.constK;
    1.34  
    1.35  
    1.36 -    fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
    1.37 -      (map Pretty.str (kind ^ ":" :: map quote (NameSpace.dest space))));
    1.38 -
    1.39      fun pretty_classes cs = Pretty.block
    1.40        (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
    1.41  
    1.42 @@ -155,7 +167,7 @@
    1.43      Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
    1.44      Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
    1.45      Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
    1.46 -    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
    1.47 +    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
    1.48      Pretty.writeln (pretty_classes classes);
    1.49      Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
    1.50      Pretty.writeln (pretty_default default);
     2.1 --- a/src/Pure/pure_thy.ML	Mon Dec 29 14:30:38 1997 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Mon Dec 29 14:31:20 1997 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4        if ! long_names then name else NameSpace.extern space name;
     2.5      val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
     2.6    in
     2.7 -    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
     2.8 +    Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
     2.9      Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
    2.10    end;
    2.11