printing of cases

--- a/src/Pure/Isar/code.ML	Thu Jan 14 17:47:39 2010 +0100
+++ b/src/Pure/Isar/code.ML	Thu Jan 14 17:47:39 2010 +0100
@@ -746,6 +746,10 @@
                           :: Pretty.str "of"
                           :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
           );
+    fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
+      | pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
+          Pretty.str (string_of_const thy const), Pretty.str "with",
+          (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
     val eqns = the_eqns exec
       |> Symtab.dest
       |> (map o apfst) (string_of_const thy)
@@ -755,18 +759,26 @@
       |> Symtab.dest
       |> map (fn (dtco, (_, (vs, cos)) :: _) =>
           (string_of_typ thy (Type (dtco, map TFree vs)), cos))
-      |> sort (string_ord o pairself fst)
+      |> sort (string_ord o pairself fst);
+    val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
+    val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
   in
     (Pretty.writeln o Pretty.chunks) [
       Pretty.block (
-        Pretty.str "code equations:"
-        :: Pretty.fbrk
+        Pretty.str "code equations:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_eqns) eqns
       ),
       Pretty.block (
-        Pretty.str "datatypes:"
-        :: Pretty.fbrk
+        Pretty.str "datatypes:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_dtyp) dtyps
+      ),
+      Pretty.block (
+        Pretty.str "cases:" :: Pretty.fbrk
+        :: (Pretty.fbreaks o map pretty_case) cases
+      ),
+      Pretty.block (
+        Pretty.str "undefined:" :: Pretty.fbrk
+        :: (Pretty.commas o map (Pretty.str o string_of_const thy)) undefineds
       )
     ]
   end;