proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
authorwenzelm
Sun, 29 Dec 2024 15:49:11 +0100
changeset 81692 442af2d573f9
parent 81691 6a8d6e7d3ebe
child 81693 84f1951bcc3c
proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
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)