# HG changeset patch
# User haftmann
# Date 1284986214 -7200
# Node ID baa049cba98b627cedbf45a7b5dd8407ba57f1f4
# Parent  386576a416ea3561383afe476d36e88f6decbdd7
use buffers instead of string concatenation

diff -r 386576a416ea -r baa049cba98b src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Sep 20 14:36:54 2010 +0200
@@ -130,32 +130,30 @@
 fun markup_stmt name = Print_Mode.setmp [code_presentationN]
   (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
 
-fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
-      implode (map (filter_presentation presentation_names
-        (selected orelse (name = code_presentationN
-          andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
-  | filter_presentation presentation_names selected (XML.Text s) =
-      if selected then s else "";
-
-fun maps_string s f [] = ""
-  | maps_string s f (x :: xs) =
+fun filter_presentation [] tree =
+      Buffer.empty
+      |> fold XML.add_content tree 
+      |> Buffer.add "\n"
+  | filter_presentation presentation_names tree =
       let
-        val s1 = f x;
-        val s2 = maps_string s f xs;
-      in if s1 = "" then s2
-        else if s2 = "" then s1
-        else s1 ^ s ^ s2
-      end;
-
-fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs
-  | plain_text (XML.Text s) = s
+        fun is_selected (name, attrs) = 
+          name = code_presentationN
+          andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
+        fun add_content_with_space tree (is_first, buf) =
+          buf
+          |> not is_first ? Buffer.add "\n\n"
+          |> XML.add_content tree
+          |> pair false;
+        fun filter (XML.Elem (name_attrs, xs)) =
+              fold (if is_selected name_attrs then add_content_with_space else filter) xs
+          | filter (XML.Text s) = I;
+      in snd (fold filter tree (true, Buffer.empty)) end;
 
 fun format presentation_names width =
   Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
   #> YXML.parse_body
-  #> (if null presentation_names then maps_string "" plain_text
-      else maps_string "\n\n" (filter_presentation presentation_names false))
-  #> suffix "\n";
+  #> filter_presentation presentation_names
+  #> Buffer.content;
 
 
 (** names and variable name contexts **)