diff -r d2522bb4db1b -r 4671d29feb00 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Nov 14 17:46:41 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sun Nov 14 20:15:28 2021 +0100
@@ -44,6 +44,8 @@
   val no_text: Text = Text("")
   val newline: Text = Text("\n")
 
+  def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
+
 
   /* name space */