# HG changeset patch
# User wenzelm
# Date 1572688613 -3600
# Node ID e5e34bd28257ee532bbc79e8154d20d7426f0de0
# Parent  64a20b562e6363eb74b4ebe6237f9dbb8854a29f
clarified signature;

diff -r 64a20b562e63 -r e5e34bd28257 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Nov 02 10:43:11 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Nov 02 10:56:53 2019 +0100
@@ -20,7 +20,7 @@
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
-  val buffer_body: XML.body -> Buffer.T -> Buffer.T
+  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
@@ -65,18 +65,20 @@
 
 (* output *)
 
-fun buffer_attrib (a, x) =
-  Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+fun traverse string =
+  let
+    fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
+    fun tree (XML.Elem ((name, atts), ts)) =
+          string XY #> string name #> fold attrib atts #> string X #>
+          fold tree ts #>
+          string XYX
+      | tree (XML.Text s) = string s;
+  in tree end;
 
-fun buffer_body ts = fold buffer ts
-and buffer (XML.Elem ((name, atts), ts)) =
-      Buffer.add XY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add X #>
-      buffer_body ts #>
-      Buffer.add XYX
-  | buffer (XML.Text s) = Buffer.add s
+val buffer = traverse Buffer.add;
 
-fun chunks_of_body body = Buffer.empty |> buffer_body body |> Buffer.chunks;
-fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
+fun chunks_of_body body = Buffer.empty |> fold buffer body |> Buffer.chunks;
+fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content;
 val string_of = string_of_body o single;
 
 
diff -r 64a20b562e63 -r e5e34bd28257 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Nov 02 10:43:11 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sat Nov 02 10:56:53 2019 +0100
@@ -129,8 +129,8 @@
   if Buffer.is_empty buffer then ()
   else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer);
 
-fun export_body thy name elems =
-  export_buffer thy name (YXML.buffer_body elems Buffer.empty);
+fun export_body thy name body =
+  export_buffer thy name (fold YXML.buffer body Buffer.empty);
 
 
 (* presentation *)
diff -r 64a20b562e63 -r e5e34bd28257 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 02 10:43:11 2019 +0100
+++ b/src/Pure/proofterm.ML	Sat Nov 02 10:56:53 2019 +0100
@@ -2150,9 +2150,8 @@
         val encode_term = encode_standard_term consts;
         val encode_proof = encode_standard_proof consts;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
-    val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
-    chunks |> Export.export_params
+    YXML.chunks_of_body xml |> Export.export_params
      {theory = thy,
       binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
       executable = false,