# HG changeset patch
# User wenzelm
# Date 1372019510 -7200
# Node ID c03090937c3bb7f3a1af7b56d5eca6df57ebd3f4
# Parent  7fa1245f50df1a43e0cc1531bc619a8a9bd2716c
tuned message -- more markup;

diff -r 7fa1245f50df -r c03090937c3b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Jun 23 21:40:56 2013 +0200
+++ b/etc/isar-keywords.el	Sun Jun 23 22:31:50 2013 +0200
@@ -183,7 +183,6 @@
     "print_classes"
     "print_codeproc"
     "print_codesetup"
-    "print_coercion_maps"
     "print_coercions"
     "print_commands"
     "print_context"
@@ -413,7 +412,6 @@
     "print_classes"
     "print_codeproc"
     "print_codesetup"
-    "print_coercion_maps"
     "print_coercions"
     "print_commands"
     "print_context"
diff -r 7fa1245f50df -r c03090937c3b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jun 23 21:40:56 2013 +0200
+++ b/src/HOL/HOL.thy	Sun Jun 23 22:31:50 2013 +0200
@@ -7,8 +7,8 @@
 theory HOL
 imports Pure "~~/src/Tools/Code_Generator"
 keywords
-  "try" "solve_direct" "quickcheck"
-    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
+  "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
+    "print_induct_rules" :: diag and
   "quickcheck_params" :: thy_decl
 begin
 
diff -r 7fa1245f50df -r c03090937c3b src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Jun 23 21:40:56 2013 +0200
+++ b/src/Tools/subtyping.ML	Sun Jun 23 22:31:50 2013 +0200
@@ -10,7 +10,6 @@
   val add_type_map: term -> Context.generic -> Context.generic
   val add_coercion: term -> Context.generic -> Context.generic
   val print_coercions: Proof.context -> unit
-  val print_coercion_maps: Proof.context -> unit
   val setup: theory -> theory
 end;
 
@@ -26,7 +25,7 @@
   {coes: (term * ((typ list * typ list) * term list)) Symreltab.table,  (*coercions table*)
    (*full coercions graph - only used at coercion declaration/deletion*)
    full_graph: int Graph.T,
-   (*coercions graph restricted to base types - for efficiency reasons strored in the context*)
+   (*coercions graph restricted to base types - for efficiency reasons stored in the context*)
    coes_graph: int Graph.T,
    tmaps: (term * variance list) Symtab.table,  (*map functions*)
    coerce_args: coerce_arg list Symtab.table  (*special constants with non-coercible arguments*)};
@@ -326,7 +325,7 @@
             val tye_idx'' = strong_unify ctxt (U --> V, T) (tye, idx + 2)
               handle NO_UNIFIER (msg, _) => error (gen_msg err msg);
             val error_pack = (bs, t $ u, U, V, U');
-          in 
+          in
             if coerce'
             then (V, tye_idx'', ((U', U), error_pack) :: cs'')
             else (V,
@@ -820,7 +819,7 @@
                     (if coerce' then "\nLocal coercion insertion on the operand failed:\n"
                     else "\nLocal coercion insertion on the operand disallowed:\n");
                   val (u'', U', tye_idx') =
-                    if coerce' then 
+                    if coerce' then
                       let val co = gen_coercion ctxt err' tye' (U, W);
                       in inf coerce' bs (if is_identity co then u else co $ u) (tye', idx') end
                     else (u, U, (tye', idx'));
@@ -1030,32 +1029,33 @@
 fun print_coercions ctxt =
   let
     fun separate _ [] = ([], [])
-      | separate P (x::xs) = (if P x then apfst else apsnd) (cons x) (separate P xs);
+      | separate P (x :: xs) = (if P x then apfst else apsnd) (cons x) (separate P xs);
     val (simple, complex) =
       separate (fn (_, (_, ((Ts, Us), _))) => null Ts andalso null Us)
         (Symreltab.dest (coes_of ctxt));
-    fun show_coercion ((a, b), (t, ((Ts, Us), _))) = Pretty.block [
-      Syntax.pretty_typ ctxt (Type (a, Ts)),
-      Pretty.brk 1, Pretty.str "<:", Pretty.brk 1,
-      Syntax.pretty_typ ctxt (Type (b, Us)),
-      Pretty.brk 3, Pretty.block [Pretty.str "using", Pretty.brk 1,
-      Pretty.quote (Syntax.pretty_term ctxt t)]];
+    fun show_coercion ((a, b), (t, ((Ts, Us), _))) =
+      Pretty.item [Pretty.block
+       [Syntax.pretty_typ ctxt (Type (a, Ts)), Pretty.brk 1,
+        Pretty.str "<:", Pretty.brk 1,
+        Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3,
+        Pretty.block
+         [Pretty.keyword "using", Pretty.brk 1,
+          Pretty.quote (Syntax.pretty_term ctxt t)]]];
+
+    val type_space = Proof_Context.type_space ctxt;
+    val tmaps =
+      sort (Name_Space.extern_ord ctxt type_space o pairself #1)
+        (Symtab.dest (tmaps_of ctxt));
+    fun show_map (x, (t, _)) =
+      Pretty.block
+       [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
+        Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
   in
-    Pretty.big_list "Coercions:"
-    [Pretty.big_list "between base types:" (map show_coercion simple),
-     Pretty.big_list "other:" (map show_coercion complex)]
-    |> Pretty.writeln
-  end;
+   [Pretty.big_list "coercions between base types:" (map show_coercion simple),
+    Pretty.big_list "other coercions:" (map show_coercion complex),
+    Pretty.big_list "coercion maps:" (map show_map tmaps)]
+  end |> Pretty.chunks |> Pretty.writeln;
 
-fun print_coercion_maps ctxt =
-  let
-    fun show_map (x, (t, _)) = Pretty.block [
-      Pretty.str x, Pretty.str ":", Pretty.brk 1,
-      Pretty.quote (Syntax.pretty_term ctxt t)];
-  in
-    Pretty.big_list "Coercion maps:" (map show_map (Symtab.dest (tmaps_of ctxt)))
-    |> Pretty.writeln
-  end;
 
 (* theory setup *)
 
@@ -1082,10 +1082,8 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
-    (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
-val _ =
-  Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
-    (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
+  Outer_Syntax.improper_command @{command_spec "print_coercions"}
+    "print information about coercions"
+    (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
 
 end;