diff -r 2e610951f79a -r ff11af12dfdd src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 12:32:38 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 12:33:38 2019 +0100
@@ -35,6 +35,8 @@
     | Text of string
   type body = tree list
   val blob: string list -> body
+  val is_empty: tree -> bool
+  val is_empty_body: body -> bool
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
@@ -78,6 +80,11 @@
 
 val blob = map Text;
 
+fun is_empty (Text "") = true
+  | is_empty _ = false;
+
+val is_empty_body = forall is_empty;
+
 
 (* wrapped elements *)