--- 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)
--- 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)
})
--- 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
--- 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 */