320 in fmt (prune prt) Buffer.empty end; |
320 in fmt (prune prt) Buffer.empty end; |
321 |
321 |
322 (*ML toplevel pretty printing*) |
322 (*ML toplevel pretty printing*) |
323 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = |
323 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = |
324 let |
324 let |
325 fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) |
325 fun pp (Block (m, prts, ind, _)) = |
|
326 let val (bg, en) = Markup.output m |
|
327 in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end |
326 | pp (String (s, _)) = put_str s |
328 | pp (String (s, _)) = put_str s |
327 | pp (Break (false, wd)) = put_brk wd |
329 | pp (Break (false, wd)) = put_brk wd |
328 | pp (Break (true, _)) = put_fbrk () |
330 | pp (Break (true, _)) = put_fbrk () |
329 and pp_lst [] = () |
331 and pp_lst [] = () |
330 | pp_lst (prt :: prts) = (pp prt; pp_lst prts); |
332 | pp_lst (prt :: prts) = (pp prt; pp_lst prts); |