# HG changeset patch
# User wenzelm
# Date 1218808250 -7200
# Node ID 10c927e4abf57ccb046c854313b81b235bf54595
# Parent  e506f0c6d3f068466225b1a8063e8009adc34895
output_markup: check Markup.is_none;

diff -r e506f0c6d3f0 -r 10c927e4abf5 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 *)
diff -r e506f0c6d3f0 -r 10c927e4abf5 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Fri Aug 15 15:50:49 2008 +0200
+++ b/src/Pure/General/yxml.ML	Fri Aug 15 15:50:50 2008 +0200
@@ -42,8 +42,9 @@
 
 (* output *)
 
-fun output_markup (name, atts) =
-  (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+fun output_markup (markup as (name, atts)) =
+  if Markup.is_none markup then ("", "")
+  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =
   let val (pre, post) = output_markup (name, atts)