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