# HG changeset patch # User haftmann # Date 1263487659 -3600 # Node ID 0d6a2ae86525c4be76aba62d7d6b30b5478b5ae5 # Parent 9b12b0824bfe376dbd4fdf40c5bc8e2e0e86497e printing of cases diff -r 9b12b0824bfe -r 0d6a2ae86525 src/Pure/Isar/code.ML --- 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;