# HG changeset patch
# User wenzelm
# Date 1735481706 -3600
# Node ID 6c3de898b055769998d2684212116151b05991e6
# Parent  e8412ab83eaf0d1a90dbb4a901c509bf6f333cfb
tuned signature;

diff -r e8412ab83eaf -r 6c3de898b055 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Dec 29 15:05:16 2024 +0100
+++ b/src/Pure/General/pretty.scala	Sun Dec 29 15:15:06 2024 +0100
@@ -69,7 +69,12 @@
     indent: Int,
     body: List[Tree],
     length: Double
-  ) extends Tree
+  ) extends Tree {
+    def no_markup: Boolean = markup.is_empty && markup_body.isEmpty
+    def markup_elem(body: XML.Body): XML.Elem =
+      if (markup_body.isEmpty) XML.Elem(markup, body)
+      else XML.Wrapped_Elem(markup, markup_body.get, body)
+  }
   private case class Break(force: Boolean, width: Int, indent: Int) extends Tree {
     def length: Double = width.toDouble
   }
@@ -189,19 +194,19 @@
           val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts
           format(ts1, blockin, after, btext1)
 
-        case Block(markup, markup_body, _, consistent, indent, body, blen) :: ts =>
-          val pos1 = (text.pos + indent).ceil.toInt
+        case (block: Block) :: ts =>
+          val pos1 = (text.pos + block.indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 = if (pos1 < emergencypos) pos1 else pos2
           val after1 = break_dist(ts, after)
-          val body1 = if (consistent && text.pos + blen > margin - after1) force_all(body) else body
+          val body1 =
+            if (block.consistent && text.pos + block.length > margin - after1) force_all(block.body)
+            else block.body
           val btext1 =
-            if (markup.is_empty && markup_body.isEmpty) format(body1, blockin1, after1, text)
+            if (block.no_markup) format(body1, blockin1, after1, text)
             else {
               val btext = format(body1, blockin1, after1, text.reset)
-              val elem =
-                if (markup_body.isEmpty) XML.Elem(markup, btext.content)
-                else XML.Wrapped_Elem(markup, markup_body.get, btext.content)
+              val elem = block.markup_elem(btext.content)
               btext.set(elem :: text.tx)
             }
           val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts