1291 fun prt_asm (b, ts) = Pretty.block (Pretty.breaks |
1291 fun prt_asm (b, ts) = Pretty.block (Pretty.breaks |
1292 ((if Binding.is_empty b then [] |
1292 ((if Binding.is_empty b then [] |
1293 else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); |
1293 else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); |
1294 |
1294 |
1295 fun prt_sect _ _ _ [] = [] |
1295 fun prt_sect _ _ _ [] = [] |
1296 | prt_sect s sep prt xs = |
1296 | prt_sect head sep prt xs = |
1297 [Pretty.block (Pretty.breaks (Pretty.str s :: |
1297 [Pretty.block (Pretty.breaks (head :: |
1298 flat (separate sep (map (single o prt) xs))))]; |
1298 flat (separate sep (map (single o prt) xs))))]; |
1299 in |
1299 in |
1300 Pretty.block (Pretty.fbreaks |
1300 Pretty.block (Pretty.fbreaks |
1301 (Pretty.str (name ^ ":") :: |
1301 (Pretty.str (name ^ ":") :: |
1302 prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @ |
1302 prt_sect (Pretty.keyword1 "fix") [] (Pretty.str o Binding.name_of o fst) fixes @ |
1303 prt_sect "let" [Pretty.str "and"] prt_let |
1303 prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let |
1304 (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ |
1304 (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ |
1305 (if forall (null o #2) asms then [] |
1305 (if forall (null o #2) asms then [] |
1306 else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @ |
1306 else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @ |
1307 prt_sect "subcases:" [] (Pretty.str o fst) cs)) |
1307 prt_sect (Pretty.str "subcases:") [] (Pretty.str o fst) cs)) |
1308 end; |
1308 end; |
1309 |
1309 |
1310 in |
1310 in |
1311 |
1311 |
1312 fun pretty_cases ctxt = |
1312 fun pretty_cases ctxt = |