tuned;
authorwenzelm
Sun, 29 Dec 2024 15:39:01 +0100
changeset 81691 6a8d6e7d3ebe
parent 81690 6e19d0ebff8a
child 81692 442af2d573f9
tuned;
src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Dec 29 15:34:28 2024 +0100
+++ b/src/Pure/General/pretty.scala	Sun Dec 29 15:39:01 2024 +0100
@@ -166,8 +166,8 @@
 
     def make_tree(inp: XML.Body): List[Tree] =
       inp flatMap {
-        case XML.Wrapped_Elem(markup, body1, body2) =>
-          List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1)))
+        case XML.Wrapped_Elem(markup, markup_body, body) =>
+          List(make_block(make_tree(body), markup = markup, markup_body = Some(markup_body)))
         case XML.Elem(markup, body) =>
           markup match {
             case Markup.Block(consistent, indent) =>