diff -r 6a8d6e7d3ebe -r 442af2d573f9 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Sun Dec 29 15:39:01 2024 +0100 +++ b/src/Pure/General/pretty.scala Sun Dec 29 15:49:11 2024 +0100 @@ -167,7 +167,8 @@ def make_tree(inp: XML.Body): List[Tree] = inp flatMap { case XML.Wrapped_Elem(markup, markup_body, body) => - List(make_block(make_tree(body), markup = markup, markup_body = Some(markup_body))) + List(make_block(make_tree(body), + markup = markup, markup_body = Some(markup_body), open_block = true)) case XML.Elem(markup, body) => markup match { case Markup.Block(consistent, indent) => @@ -190,7 +191,8 @@ case (block: Block) :: ts if block.open_block => val btext = format(block.body, blockin, break_dist(ts, after), text.reset) - val btext1 = btext.set(XML.Elem(block.markup, btext.content) :: text.tx) + val elem = block.markup_elem(btext.content) + val btext1 = btext.set(elem :: text.tx) val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts format(ts1, blockin, after, btext1)