# HG changeset patch
# User wenzelm
# Date 1365621635 -7200
# Node ID ecd34f8632421272691c6080e40200e4f44bdc19
# Parent  69e3bc394f09c9af4d2d5a7d176f80439e890729
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;

diff -r 69e3bc394f09 -r ecd34f863242 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 10 20:58:01 2013 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 10 21:20:35 2013 +0200
@@ -8,8 +8,7 @@
 imports Pure "~~/src/Tools/Code_Generator"
 keywords
   "try" "solve_direct" "quickcheck"
-    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" 
-    "print_case_translations":: diag and
+    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
   "quickcheck_params" :: thy_decl
 begin
 
diff -r 69e3bc394f09 -r ecd34f863242 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Apr 10 20:58:01 2013 +0200
+++ b/src/HOL/Inductive.thy	Wed Apr 10 21:20:35 2013 +0200
@@ -9,7 +9,7 @@
 keywords
   "inductive" "coinductive" :: thy_decl and
   "inductive_cases" "inductive_simps" :: thy_script and "monos" and
-  "print_inductives" :: diag and
+  "print_inductives" "print_case_translations" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 begin
diff -r 69e3bc394f09 -r ecd34f863242 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 20:58:01 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:20:35 2013 +0200
@@ -582,15 +582,15 @@
   let
     val cases = Symtab.dest (cases_of ctxt);
     fun show_case (_, data as (comb, ctrs)) =
-      Pretty.big_list
-        (Pretty.string_of (Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"]))
-        [Pretty.block [Pretty.brk 3, Pretty.block
+      (Pretty.block o Pretty.fbreaks)
+        [Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"],
+         Pretty.block [Pretty.brk 3, Pretty.block
           [Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]],
-        Pretty.block [Pretty.brk 3, Pretty.block
+         Pretty.block [Pretty.brk 3, Pretty.block
           [Pretty.str "constructors:", Pretty.brk 1,
-             Pretty.list "" "" (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs)]]];
+            Pretty.block (Pretty.commas (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs))]]];
   in
-    Pretty.big_list "Case translations:" (map show_case cases)
+    Pretty.big_list "case translations:" (map show_case cases)
     |> Pretty.writeln
   end;