changeset 69867 | 3fd9298dd200 |
parent 67896 | 00797fb82869 |
child 71601 | 97ccf48c2f0c |
--- a/src/Pure/General/pretty.scala Tue Mar 05 16:40:12 2019 +0100 +++ b/src/Pure/General/pretty.scala Tue Mar 05 18:44:02 2019 +0100 @@ -25,7 +25,7 @@ def brk(width: Int, indent: Int = 0): XML.Tree = XML.Elem(Markup.Break(width, indent), spaces(width)) - val fbrk: XML.Tree = XML.Text("\n") + val fbrk: XML.Tree = XML.newline def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts) val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)