# HG changeset patch
# User wenzelm
# Date 1572694418 -3600
# Node ID ff11af12dfdd5354fe642f365839a14eb499bc8a
# Parent  2e610951f79a152381875c3837c21bf778d3f1c7
clarified signature;

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 *)
 
diff -r 2e610951f79a -r ff11af12dfdd src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Nov 02 12:32:38 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sat Nov 02 12:33:38 2019 +0100
@@ -126,7 +126,7 @@
     if Options.bool (#options context) "export_theory" then f context thy else ()));
 
 fun export_body thy name body =
-  if null body then ()
+  if XML.is_empty_body body then ()
   else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;