src/Pure/General/pretty.scala
changeset 65130 695930882487
parent 62820 5c678ee5d34a
child 67547 aefe7a7b330a
--- a/src/Pure/General/pretty.scala	Mon Mar 06 16:47:52 2017 +0100
+++ b/src/Pure/General/pretty.scala	Mon Mar 06 17:05:57 2017 +0100
@@ -26,6 +26,7 @@
     XML.Elem(Markup.Break(width, indent), spaces(width))
 
   val fbrk: XML.Tree = XML.Text("\n")
+  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