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