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