# HG changeset patch # User wenzelm # Date 1735483141 -3600 # Node ID 6a8d6e7d3ebe07145db2c38b9bca390948bbf51f # Parent 6e19d0ebff8a3e15c2e29c3e1a21b90755cc1b2a tuned; diff -r 6e19d0ebff8a -r 6a8d6e7d3ebe 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) =>