# HG changeset patch
# User wenzelm
# Date 1551807842 -3600
# Node ID 3fd9298dd2008316e7c113f6579571079d529f5e
# Parent  01732226987a4b720101a53afd45f2bac7d39da2
tuned;

diff -r 01732226987a -r 3fd9298dd200 src/Pure/General/pretty.scala
--- 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)
diff -r 01732226987a -r 3fd9298dd200 src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Tue Mar 05 16:40:12 2019 +0100
+++ b/src/Pure/General/rdf.scala	Tue Mar 05 18:44:02 2019 +0100
@@ -39,8 +39,7 @@
   def triples(args: List[Triple]): XML.Body =
     args.groupBy(_.subject).toList.map(
       { case (subject, ts) =>
-          val nl = XML.Text("\n")
-          val body = nl :: ts.flatMap(t => List(t.property, nl))
+          val body = XML.newline :: ts.flatMap(t => List(t.property, XML.newline))
           description(subject, body)
       })
 
diff -r 01732226987a -r 3fd9298dd200 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Tue Mar 05 16:40:12 2019 +0100
+++ b/src/Pure/PIDE/prover.scala	Tue Mar 05 18:44:02 2019 +0100
@@ -23,7 +23,7 @@
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
         args.map(s =>
-          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   }
 
   class Output(val message: XML.Elem) extends Message
diff -r 01732226987a -r 3fd9298dd200 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Mar 05 16:40:12 2019 +0100
+++ b/src/Pure/PIDE/xml.scala	Tue Mar 05 18:44:02 2019 +0100
@@ -34,6 +34,8 @@
   def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
   def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
 
+  val newline: Text = Text("\n")
+
 
   /* name space */