1344 |
1344 |
1345 fun prt_let (xi, t) = Pretty.block |
1345 fun prt_let (xi, t) = Pretty.block |
1346 [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, |
1346 [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, |
1347 Pretty.quote (prt_term t)]; |
1347 Pretty.quote (prt_term t)]; |
1348 |
1348 |
1349 fun prt_asm (b, ts) = Pretty.block (Pretty.breaks |
1349 fun prt_asm (b, ts) = |
1350 ((if Binding.is_empty b then [] |
1350 Pretty.block (Pretty.breaks |
1351 else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); |
1351 ((if Binding.is_empty b then [] else [Binding.pretty b, Pretty.str ":"]) @ |
|
1352 map (Pretty.quote o prt_term) ts)); |
1352 |
1353 |
1353 fun prt_sect _ _ _ [] = [] |
1354 fun prt_sect _ _ _ [] = [] |
1354 | prt_sect head sep prt xs = |
1355 | prt_sect head sep prt xs = |
1355 [Pretty.block (Pretty.breaks (head :: |
1356 [Pretty.block (Pretty.breaks (head :: |
1356 flat (separate sep (map (single o prt) xs))))]; |
1357 flat (separate sep (map (single o prt) xs))))]; |