Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
output_markup: check Markup.is_none;
authorwenzelm
Fri, 15 Aug 2008 15:50:50 +0200
changeset 27884 10c927e4abf5
parent 27883 e506f0c6d3f0
child 27885 76b51cd0a37c
output_markup: check Markup.is_none;
src/Pure/General/xml.ML file | annotate | diff | comparison | revisions
src/Pure/General/yxml.ML file | annotate | diff | comparison | revisions 
--- 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 *)
--- 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)
isabelle