# HG changeset patch
# User wenzelm
# Date 1364215064 -3600
# Node ID b4f7e6734acc8ee0fdc636147c781f186d664904
# Parent  22fd3605c7a29340233b5be8e60da8b29bd15ec8
tuned print_classes: more standard order, markup, formatting;
uniform printing of minimal supersort/classrel;

diff -r 22fd3605c7a2 -r b4f7e6734acc src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 25 11:05:07 2013 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 25 13:37:44 2013 +0100
@@ -31,6 +31,8 @@
   val names_unique_raw: Config.raw
   val names_unique: bool Config.T
   val extern: Proof.context -> T -> string -> xstring
+  val extern_ord: Proof.context -> T -> string * string -> order
+  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
@@ -194,6 +196,10 @@
     else ext (get_accesses space name)
   end;
 
+fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
+
+fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
+
 
 (* modify internals *)
 
diff -r 22fd3605c7a2 -r b4f7e6734acc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Mar 25 11:05:07 2013 +0100
+++ b/src/Pure/Isar/class.ML	Mon Mar 25 13:37:44 2013 +0100
@@ -161,34 +161,50 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
+
+    val class_space = Proof_Context.class_space ctxt;
+    val type_space = Proof_Context.type_space ctxt;
+    val const_space = Proof_Context.const_space ctxt;
+
     val arities =
       Symtab.empty
       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
            Symtab.map_default (class, []) (insert (op =) tyco)) arities)
              (Sorts.arities_of algebra);
-    val the_arities = these o Symtab.lookup arities;
-    fun mk_arity class tyco =
+
+    fun prt_supersort class =
+      Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class));
+
+    fun prt_arity class tyco =
       let
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
-    fun mk_param (c, ty) =
-      Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
-        Syntax.string_of_typ ctxt (Type.strip_sorts_dummy ty));
-    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
-      (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
-      (SOME o Pretty.block) [Pretty.str "supersort: ",
-        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
-      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
-          (Pretty.str "parameters:" :: ps)) o map mk_param
-        o these o Option.map #params o try (AxClass.get_info thy)) class,
-      (SOME o Pretty.block o Pretty.breaks) [
-        Pretty.str "instances:",
-        Pretty.list "" "" (map (mk_arity class) (the_arities class))
-      ]
-    ]
+
+    fun prt_param (c, ty) =
+      Pretty.block
+       [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
+        Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
+
+    fun prt_entry class =
+      Pretty.block
+        ([Pretty.command "class", Pretty.brk 1,
+          Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
+          Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
+          (case try (AxClass.get_info thy) class of
+            NONE => []
+          | SOME {params, ...} =>
+              [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
+          (case Symtab.lookup arities class of
+            NONE => []
+          | SOME ars =>
+              [Pretty.fbrk, Pretty.big_list "instances:"
+                (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))]));
   in
-    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
-      o map mk_entry o Sorts.all_classes) algebra
+    Sorts.all_classes algebra
+    |> sort (Name_Space.extern_ord ctxt class_space)
+    |> map prt_entry
+    |> Pretty.chunks2
+    |> Pretty.writeln
   end;
 
 
diff -r 22fd3605c7a2 -r b4f7e6734acc src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Mar 25 11:05:07 2013 +0100
+++ b/src/Pure/display.ML	Mon Mar 25 13:37:44 2013 +0100
@@ -122,8 +122,7 @@
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
-          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
-            Pretty.commas (map prt_cls cs));
+          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
 
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
@@ -167,13 +166,12 @@
     val extern_const = Name_Space.extern ctxt (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
-    val class_ord = string_ord o pairself (Name_Space.extern ctxt class_space);
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
       Name_Space.dest_table ctxt (class_space,
-        Symtab.make (map (fn ((c, _), cs) => (c, sort class_ord cs)) (Graph.dest classes)));
+        Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)));
     val tdecls = Name_Space.dest_table ctxt types;
     val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);