changeset 27884 | 10c927e4abf5 |
parent 26984 | d0e098e206f3 |
child 28017 | 4919bd124a58 |
--- 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 *)