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