diff -r 000bcf2524fd -r 95e0f014cd24 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Jan 02 16:12:52 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 02 16:30:43 2021 +0100
@@ -34,6 +34,7 @@
   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 no_text: Text = Text("")
   val newline: Text = Text("\n")