# HG changeset patch
# User wenzelm
# Date 1442946113 -7200
# Node ID 63875746d82d9014385cf946503f24a7991ea146
# Parent  c165f0472d57de8bab713c2577bf7cfceabcd632
tuned output;

diff -r c165f0472d57 -r 63875746d82d src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 22 18:56:25 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 22 20:21:53 2015 +0200
@@ -83,36 +83,47 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val prt_item = Defs.pretty_item ctxt;
-    fun sort_item_by f = sort (Defs.item_ord o apply2 f);
+    val const_space = Proof_Context.const_space ctxt;
+    val type_space = Proof_Context.type_space ctxt;
+    val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
+    fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
+
+    fun markup_extern_item (kind, name) =
+      let val (markup, xname) = Name_Space.markup_extern ctxt (item_space kind) name
+      in (markup, (kind, xname)) end;
+
+    fun pretty_entry ((markup, (kind, xname)), args) =
+      let
+        val prt_prefix =
+          if kind = Defs.Type then [Pretty.keyword1 "type", Pretty.brk 1] else [];
+        val prt_item = Pretty.mark_str (markup, xname);
+        val prt_args = Defs.pretty_args ctxt args;
+      in Pretty.block (prt_prefix @ [prt_item] @ prt_args) end;
+
+    fun sort_items f = sort (Defs.item_ord o apply2 (snd o f));
 
     fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds));
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_entry o fst) reds));
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
-      ([prt_item lhs, Pretty.str "  ->", Pretty.brk 2] @
-        Pretty.commas (map prt_item (sort_item_by #1 rhs)));
+      ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
+        Pretty.commas (map pretty_entry (sort_items fst rhs)));
 
-    fun pretty_restrict (const, name) =
-      Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+    fun pretty_restrict (entry, name) =
+      Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
 
-    val const_space = Proof_Context.const_space ctxt;
-    val type_space = Proof_Context.type_space ctxt;
-    val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
-
-    fun extern_item (k, c) = (k, Name_Space.extern ctxt (item_space k) c);
-    fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
-
-    val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts
+    val (reds0, (reds1, reds2)) =
+      filter_out (prune_item o #1 o #1) reducts
       |> map (fn (lhs, rhs) =>
-        (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
-      |> sort_item_by (#1 o #1)
+        (apfst markup_extern_item lhs, map (apfst markup_extern_item) (filter_out (prune_item o fst) rhs)))
+      |> sort_items (#1 o #1)
       |> List.partition (null o #2)
       ||> List.partition (Defs.plain_args o #2 o #1);
-    val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1);
+
+    val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1);
   in
     Pretty.big_list "definitions:"
       [pretty_finals reds0,
diff -r c165f0472d57 -r 63875746d82d src/Pure/defs.ML
--- a/src/Pure/defs.ML	Tue Sep 22 18:56:25 2015 +0200
+++ b/src/Pure/defs.ML	Tue Sep 22 20:21:53 2015 +0200
@@ -10,7 +10,7 @@
   datatype item_kind = Constant | Type
   type item = item_kind * string
   val item_ord: item * item -> order
-  val pretty_item: Proof.context -> item * typ list -> Pretty.T
+  val pretty_args: Proof.context -> typ list -> Pretty.T list
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -45,8 +45,7 @@
 val item_ord = prod_ord item_kind_ord string_ord;
 val fast_item_ord = prod_ord item_kind_ord fast_string_ord;
 
-val print_item_kind = fn Constant => "constant" | Type => "type";
-fun print_item (k, s) = print_item_kind k ^ " " ^ quote s;
+fun print_item (k, s) = if k = Constant then s else "type " ^ s;
 
 structure Itemtab = Table(type key = item val ord = fast_item_ord);
 
@@ -55,12 +54,12 @@
 
 type args = typ list;
 
-fun pretty_item ctxt (c, args) =
-  let
-    val prt_args =
-      if null args then []
-      else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
-  in Pretty.block (Pretty.str (print_item c) :: prt_args) end;
+fun pretty_args ctxt args =
+  if null args then []
+  else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
+
+fun pretty_entry ctxt (c, args) =
+  Pretty.block (Pretty.str (print_item c) :: pretty_args ctxt args);
 
 fun plain_args args =
   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
@@ -149,7 +148,7 @@
 
 local
 
-val prt = Pretty.string_of oo pretty_item;
+val prt = Pretty.string_of oo pretty_entry;
 fun err ctxt (c, args) (d, Us) s1 s2 =
   error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);