# HG changeset patch
# User wenzelm
# Date 1727193462 -7200
# Node ID 334625aec7a4f3d07cdf7e3dd14fc5248abad2d0
# Parent  3eca969b3c43bce3ec6194dc53ca125c5d78aab9
clarified signature;

diff -r 3eca969b3c43 -r 334625aec7a4 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Sep 24 17:41:05 2024 +0200
+++ b/src/Pure/General/pretty.scala	Tue Sep 24 17:57:42 2024 +0200
@@ -18,6 +18,8 @@
     else if (n == 1) space
     else List(XML.Text(Symbol.spaces(n)))
 
+  val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
+
   def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
     XML.Elem(Markup.Block(consistent, indent), body)
 
@@ -75,12 +77,11 @@
 
   private val FBreak = Break(true, 1, 0)
 
-  private def make_block(
-    markup: Markup,
-    markup_body: Option[XML.Body],
-    consistent: Boolean,
-    indent: Int,
-    body: List[Tree]
+  private def make_block(body: List[Tree],
+    markup: Markup = Markup.Empty,
+    markup_body: Option[XML.Body] = None,
+    consistent: Boolean = false,
+    indent: Int = 0
   ): Tree = {
     val indent1 = force_nat(indent)
 
@@ -157,18 +158,17 @@
     def make_tree(inp: XML.Body): List[Tree] =
       inp flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
-          List(make_block(markup, Some(body1), false, 0, make_tree(body2)))
+          List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1)))
         case XML.Elem(markup, body) =>
           markup match {
             case Markup.Block(consistent, indent) =>
-              List(make_block(Markup.Empty, None, consistent, indent, make_tree(body)))
+              List(make_block(make_tree(body), consistent = consistent, indent = indent))
             case Markup.Break(width, indent) =>
               List(Break(false, force_nat(width), force_nat(indent)))
             case Markup(Markup.ITEM, _) =>
-              List(make_block(Markup.Empty, None, false, 2,
-                make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
+              List(make_block(make_tree(bullet ::: body), indent = 2))
             case _ =>
-              List(make_block(markup, None, false, 0, make_tree(body)))
+              List(make_block(make_tree(body), markup = markup))
           }
         case XML.Text(text) =>
           Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))