1.1 --- a/src/Pure/General/yxml.ML Fri Aug 15 15:50:49 2008 +0200
1.2 +++ b/src/Pure/General/yxml.ML Fri Aug 15 15:50:50 2008 +0200
1.3 @@ -42,8 +42,9 @@
1.4
1.5 (* output *)
1.6
1.7 -fun output_markup (name, atts) =
1.8 - (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
1.9 +fun output_markup (markup as (name, atts)) =
1.10 + if Markup.is_none markup then ("", "")
1.11 + else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
1.12
1.13 fun element name atts body =
1.14 let val (pre, post) = output_markup (name, atts)