src/Pure/General/pretty.ML
changeset 27347 31f98eaa198d
parent 26703 c07b1a90600c
child 27350 c8adf88960ad
equal deleted inserted replaced
27346:b664e5bc95fd 27347:31f98eaa198d
   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);