src/Pure/General/xml.ML

--- a/src/Pure/General/xml.ML	Fri Aug 15 15:50:49 2008 +0200
+++ b/src/Pure/General/xml.ML	Fri Aug 15 15:50:50 2008 +0200
@@ -81,9 +81,9 @@
     else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   end;
 
-fun output_markup (name, atts) =
- (enclose "<" ">" (elem name atts),
-  enclose "</" ">" name);
+fun output_markup (markup as (name, atts)) =
+  if Markup.is_none markup then ("", "")
+  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
 (* output *)