diff -r c72fd8f1fceb -r c337c798f64c src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Apr 01 19:01:19 2021 +0200
@@ -190,6 +190,7 @@
 
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
+  def text(s: String): String = string_of_tree(XML.Text(s))
 
 
   /** cache **/