# HG changeset patch
# User wenzelm
# Date 1661172494 -7200
# Node ID 97445e2084194fc2d53477d14c5012094ff5b67b
# Parent  515b17021c917eb7495eb76cb654933499a06f35
tuned signature;
more operations;

diff -r 515b17021c91 -r 97445e208419 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Aug 22 13:29:06 2022 +0200
+++ b/src/Pure/General/pretty.scala	Mon Aug 22 14:48:14 2022 +0200
@@ -18,10 +18,8 @@
     else if (n == 1) space
     else List(XML.Text(Symbol.spaces(n)))
 
-  def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+  def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
     XML.Elem(Markup.Block(consistent, indent), body)
-  def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
-  def block(body: XML.Body): XML.Tree = block(2, body)
 
   def brk(width: Int, indent: Int = 0): XML.Tree =
     XML.Elem(Markup.Break(width, indent), spaces(width))
@@ -30,7 +28,18 @@
   def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
 
   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
-  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
+  def separate(ts: List[XML.Tree], sep: XML.Body = Separator): XML.Body =
+    Library.separate(sep, ts.map(List(_))).flatten
+
+  val comma: XML.Body = List(XML.Text(","), brk(1))
+  def commas(ts: List[XML.Tree]): XML.Body = separate(ts, sep = comma)
+
+  def `enum`(ts: List[XML.Tree],
+    bg: String = "(",
+    en: String = ")",
+    sep: XML.Body = comma,
+    indent: Int = 2
+  ): XML.Tree = Pretty.block(XML.enclose(bg, en, separate(ts, sep = sep)), indent = indent)
 
 
   /* text metric -- standardized to width of space */
diff -r 515b17021c91 -r 97445e208419 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Aug 22 13:29:06 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Aug 22 14:48:14 2022 +0200
@@ -659,7 +659,7 @@
             Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
-            Some(info + (r0, true, Pretty.block(0, body)))
+            Some(info + (r0, true, Pretty.block(body, indent = 0)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))