--- 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 *)
--- 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;