--- 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 */
--- 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)))