# 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)))