src/Pure/General/pretty.scala
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)