diff -r d5ad89fda714 -r ff3dd5ba47d0 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sun Oct 27 11:13:42 2024 +0100 +++ b/src/Pure/General/pretty.ML Sun Oct 27 11:22:34 2024 +0100 @@ -368,7 +368,6 @@ | break_dist ([], after) = after; val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | prt => prt; -val force_all = map force_break; (*Search for the next break (at this or higher levels) and force it to occur.*) fun force_next [] = [] @@ -400,9 +399,9 @@ fun format ([], _, _) text = text | format (prt :: prts, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = (case prt of - Block {markup = (bg, en), open_block = true, body = bes, ...} => - format (Out bg :: bes @ Out en :: prts, block, after) text - | Block {markup = (bg, en), consistent, indent, body = bes, length = blen, ...} => + Block {markup = (bg, en), open_block = true, body, ...} => + format (Out bg :: body @ Out en :: prts, block, after) text + | Block {markup = (bg, en), consistent, indent, body, length = blen, ...} => let val pos' = pos + indent; val pos'' = pos' mod emergencypos; @@ -410,10 +409,10 @@ if pos' < emergencypos then (ind |> blanks_buffer indent, pos') else (blanks_buffer pos'' Buffer.empty, pos''); val d = break_dist (prts, after) - val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes; + val body' = body |> (consistent andalso pos + blen > margin - d) ? map force_break; val btext: text = text |> control bg - |> format (bes', block', d) + |> format (body', block', d) |> control en; (*if this block was broken then force the next break*) val prts' = if nl < #nl btext then force_next prts else prts; @@ -444,22 +443,22 @@ let val ops = symbolic_output_ops; - fun markup_bytes m body = + fun markup_bytes m output_body = let val (bg, en) = #markup ops (YXML.output_markup m) - in Bytes.add bg #> body #> Bytes.add en end; + in Bytes.add bg #> output_body #> Bytes.add en end; - fun out (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en - | out (Block {markup = (bg, en), open_block = true, body = prts, ...}) = - Bytes.add bg #> fold out prts #> Bytes.add en - | out (Block {markup = (bg, en), consistent, indent, body = prts, ...}) = + fun output (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en + | output (Block {markup = (bg, en), open_block = true, body, ...}) = + Bytes.add bg #> fold output body #> Bytes.add en + | output (Block {markup = (bg, en), consistent, indent, body, ...}) = let val block_markup = Markup.block {consistent = consistent, indent = indent} - in Bytes.add bg #> markup_bytes block_markup (fold out prts) #> Bytes.add en end - | out (Break (false, wd, ind)) = + in Bytes.add bg #> markup_bytes block_markup (fold output body) #> Bytes.add en end + | output (Break (false, wd, ind)) = markup_bytes (Markup.break {width = wd, indent = ind}) (output_spaces_bytes ops wd) - | out (Break (true, _, _)) = Bytes.add (output_newline ops) - | out (Str (s, _)) = Bytes.add s - | out (Out s) = Bytes.add s; - in Bytes.build o out o output_tree ops false end; + | output (Break (true, _, _)) = Bytes.add (output_newline ops) + | output (Str (s, _)) = Bytes.add s + | output (Out s) = Bytes.add s; + in Bytes.build o output o output_tree ops false end; val symbolic_string_of = Bytes.content o symbolic_output; @@ -468,12 +467,12 @@ fun unformatted ops = let - fun out (Block ({markup = (bg, en), body = prts, ...})) = - Bytes.add bg #> fold out prts #> Bytes.add en - | out (Break (_, wd, _)) = output_spaces_bytes ops wd - | out (Str (s, _)) = Bytes.add s - | out (Out s) = Bytes.add s; - in Bytes.build o out o output_tree ops false end; + fun output (Block ({markup = (bg, en), body, ...})) = + Bytes.add bg #> fold output body #> Bytes.add en + | output (Break (_, wd, _)) = output_spaces_bytes ops wd + | output (Str (s, _)) = Bytes.add s + | output (Out s) = Bytes.add s; + in Bytes.build o output o output_tree ops false end; fun unformatted_string_of prt = Bytes.content (unformatted (output_ops NONE) prt);