# HG changeset patch
# User wenzelm
# Date 1572697237 -3600
# Node ID ebdfd6c43e563a541e04595a05501d9deee27ba8
# Parent  2c17fa0f51871effa0dea007a40daf6d0d1c3eff
unused;

diff -r 2c17fa0f5187 -r ebdfd6c43e56 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Nov 02 12:39:44 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Nov 02 13:20:37 2019 +0100
@@ -21,8 +21,6 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
-  val buffer: XML.tree -> Buffer.T -> Buffer.T
-  val chunks_of_body: XML.body -> string list
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
@@ -76,10 +74,7 @@
       | tree (XML.Text s) = string s;
   in tree end;
 
-val buffer = traverse Buffer.add;
-
-fun chunks_of_body body = Buffer.empty |> fold buffer body |> Buffer.chunks;
-fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content;
+fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
 val string_of = string_of_body o single;
 
 fun write_body path body =