equal
deleted
inserted
replaced
1027 |
1027 |
1028 fun pretty_cases (ctxt as Context {cases, ...}) = |
1028 fun pretty_cases (ctxt as Context {cases, ...}) = |
1029 let |
1029 let |
1030 val prt_term = Sign.pretty_term (sign_of ctxt); |
1030 val prt_term = Sign.pretty_term (sign_of ctxt); |
1031 fun prt_let (xi, t) = Pretty.block |
1031 fun prt_let (xi, t) = Pretty.block |
1032 [prt_term (Var (xi, Term.fastype_of t)), Pretty.str " =", Pretty.brk 1, |
1032 [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, |
1033 Pretty.quote (prt_term t)]; |
1033 Pretty.quote (prt_term t)]; |
1034 |
1034 |
1035 fun prt_sect _ _ _ [] = [] |
1035 fun prt_sect _ _ _ [] = [] |
1036 | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: |
1036 | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: |
1037 flat (Library.separate sep (map (Library.single o prt) xs))))]; |
1037 flat (Library.separate sep (map (Library.single o prt) xs))))]; |