src/Pure/PIDE/yxml.ML
changeset 73556 192bcee4f8b8
parent 71456 09c850e82258
child 73557 225486d9c960
equal deleted inserted replaced
73554:c973b5300025 73556:192bcee4f8b8
    66 (* output *)
    66 (* output *)
    67 
    67 
    68 fun traverse string =
    68 fun traverse string =
    69   let
    69   let
    70     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
    70     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
    71     fun tree (XML.Elem ((name, atts), ts)) =
    71     fun tree (XML.Elem (markup as (name, atts), ts)) =
    72           string XY #> string name #> fold attrib atts #> string X #>
    72           if Markup.is_empty markup then fold tree ts
    73           fold tree ts #>
    73           else
    74           string XYX
    74             string XY #> string name #> fold attrib atts #> string X #>
       
    75             fold tree ts #>
       
    76             string XYX
    75       | tree (XML.Text s) = string s;
    77       | tree (XML.Text s) = string s;
    76   in tree end;
    78   in tree end;
    77 
    79 
    78 fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
    80 fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
    79 val string_of = string_of_body o single;
    81 val string_of = string_of_body o single;