# HG changeset patch # User wenzelm # Date 1310308264 -7200 # Node ID 152ce7114396be9cddf71f733dc9638c2fc53f50 # Parent a0c3de0573d405f4b6e9f3402fbdab4969204e0b YXML.string_of_body convenience; diff -r a0c3de0573d4 -r 152ce7114396 src/Pure/General/yxml.ML --- a/src/Pure/General/yxml.ML Sun Jul 10 16:13:37 2011 +0200 +++ b/src/Pure/General/yxml.ML Sun Jul 10 16:31:04 2011 +0200 @@ -18,6 +18,7 @@ val escape_controls: string -> string val output_markup: Markup.T -> string * string val element: string -> XML.attributes -> string list -> string + val string_of_body: XML.body -> string val string_of: XML.tree -> string val parse_body: string -> XML.body val parse: string -> XML.tree @@ -59,17 +60,20 @@ let val (pre, post) = output_markup (name, atts) in pre ^ implode body ^ post end; -fun string_of t = +fun string_of_body body = let fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x; fun tree (XML.Elem ((name, atts), ts)) = Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #> - fold tree ts #> + trees ts #> Buffer.add XYX - | tree (XML.Text s) = Buffer.add s; - in Buffer.empty |> tree t |> Buffer.content end; + | tree (XML.Text s) = Buffer.add s + and trees ts = fold tree ts; + in Buffer.empty |> trees body |> Buffer.content end; + +val string_of = string_of_body o single;