diff -r 95e514137861 -r a5c23da73fca src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Mon Nov 15 11:38:14 2021 +0100
@@ -46,6 +46,9 @@
 
   def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
 
+  def enclose(bg: String, en:String, body: Body): Body =
+    string(bg) ::: body ::: string(en)
+
 
   /* name space */