# HG changeset patch # User wenzelm # Date 1184168869 -7200 # Node ID 4868d391396182bcfee4f914971b1780e90c417e # Parent 3390bb8cf681937c918994afa8aeea6f2c357ffd Buffer.markup; diff -r 3390bb8cf681 -r 4868d3913961 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Wed Jul 11 17:47:48 2007 +0200 +++ b/src/Pure/General/pretty.ML Wed Jul 11 17:47:49 2007 +0200 @@ -299,25 +299,21 @@ (* special output *) -fun add_markup m add = - let val (bg, en) = Markup.output m - in Buffer.add bg #> add #> Buffer.add en end; - (*symbolic markup -- no formatting*) fun symbolic prt = let - fun out (Block (m, [], _, _)) = add_markup m I + fun out (Block (m, [], _, _)) = Buffer.markup m I | out (Block (m, prts, indent, _)) = - add_markup m (add_markup (Markup.block indent) (fold out prts)) + Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts)) | out (String (s, _)) = Buffer.add s - | out (Break (false, wd)) = add_markup (Markup.break wd) (Buffer.add (output_spaces wd)) - | out (Break (true, _)) = add_markup Markup.fbreak (Buffer.add (output_spaces 1)); + | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd)) + | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1)); in out prt Buffer.empty end; (*unformatted output*) fun unformatted prt = let - fun fmt (Block (m, prts, _, _)) = add_markup m (fold fmt prts) + fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts) | fmt (String (s, _)) = Buffer.add s | fmt (Break (false, wd)) = Buffer.add (output_spaces wd) | fmt (Break (true, _)) = Buffer.add (output_spaces 1);