# HG changeset patch
# User wenzelm
# Date 1630778503 -7200
# Node ID b3c65c984210933dd167025bb3332eeac5282654
# Parent  d637611b41bdef622d2338763b4ca6f0ba79f3cf
tuned signature;

diff -r d637611b41bd -r b3c65c984210 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/General/buffer.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -9,8 +9,10 @@
   type T
   val empty: T
   val is_empty: T -> bool
+  val add: string -> T -> T
   val content: T -> string
-  val add: string -> T -> T
+  val build: (T -> T) -> T
+  val build_content: (T -> T) -> string
   val output: T -> (string -> unit) -> unit
   val markup: Markup.T -> (T -> T) -> T -> T
 end;
@@ -30,6 +32,9 @@
 
 fun content (Buffer xs) = implode (rev xs);
 
+fun build (f: T -> T) = f empty;
+fun build_content f = build f |> content;
+
 fun output (Buffer xs) out = List.app out (rev xs);
 
 end;
diff -r d637611b41bd -r b3c65c984210 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/General/pretty.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -321,7 +321,7 @@
 (* special output *)
 
 (*symbolic markup -- no formatting*)
-fun symbolic prt =
+val symbolic =
   let
     fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
       | out (Block ((bg, en), consistent, indent, prts, _)) =
@@ -332,15 +332,15 @@
           Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
       | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
       | out (Str (s, _)) = Buffer.add s;
-  in out prt Buffer.empty end;
+  in Buffer.build o out end;
 
 (*unformatted output*)
-fun unformatted prt =
+val unformatted =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
       | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
       | out (Str (s, _)) = Buffer.add s;
-  in out prt Buffer.empty end;
+  in Buffer.build o out end;
 
 
 (* output interfaces *)
diff -r d637611b41bd -r b3c65c984210 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/PIDE/xml.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -110,7 +110,7 @@
         Elem (_, ts) => fold add_content ts
       | Text s => Buffer.add s));
 
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+val content_of = Buffer.build_content o fold add_content;
 
 
 (* trim blanks *)
@@ -164,9 +164,9 @@
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
-(* output *)
+(* output content *)
 
-fun buffer_of depth tree =
+fun content_depth depth =
   let
     fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
@@ -177,12 +177,11 @@
       | traverse _ (Text s) = Buffer.add (text s)
     and traverse_body 0 _ = Buffer.add "..."
       | traverse_body d ts = fold (traverse (d - 1)) ts;
-  in Buffer.empty |> traverse depth tree end;
+  in Buffer.build_content o traverse depth end;
 
-val string_of = Buffer.content o buffer_of ~1;
+val string_of = content_depth ~1;
 
-fun pretty depth tree =
-  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
 
 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
diff -r d637611b41bd -r b3c65c984210 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -85,7 +85,7 @@
 
 (* output *)
 
-fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
 val string_of = string_of_body o single;
 
 fun write_body path body =
diff -r d637611b41bd -r b3c65c984210 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Tools/Code/code_printer.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -142,10 +142,9 @@
 fun markup_stmt sym = with_presentation_marker
   (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
 
-fun filter_presentation [] tree =
-      Buffer.empty
-      |> fold XML.add_content tree
-  | filter_presentation presentation_syms tree =
+fun filter_presentation [] xml =
+      Buffer.build (fold XML.add_content xml)
+  | filter_presentation presentation_syms xml =
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
         fun is_selected (name, attrs) =
@@ -159,7 +158,7 @@
         fun filter (XML.Elem (name_attrs, xs)) =
               fold (if is_selected name_attrs then add_content_with_space else filter) xs
           | filter (XML.Text _) = I;
-      in snd (fold filter tree (true, Buffer.empty)) end;
+      in snd (fold filter xml (true, Buffer.empty)) end;
 
 fun format presentation_names width =
   with_presentation_marker (Pretty.string_of_margin width)
diff -r d637611b41bd -r b3c65c984210 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sat Sep 04 20:01:43 2021 +0200
@@ -572,11 +572,12 @@
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
 -}
 
-module Isabelle.Buffer (T, empty, add, content)
+module Isabelle.Buffer (T, empty, add, content, build, build_content)
 where
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
+import Isabelle.Library
 
 
 newtype T = Buffer [Bytes]
@@ -589,6 +590,12 @@
 
 content :: T -> Bytes
 content (Buffer bs) = Bytes.concat (reverse bs)
+
+build :: (T -> T) -> T
+build f = f empty
+
+build_content :: (T -> T) -> Bytes
+build_content f = build f |> content
 \<close>
 
 generate_file "Isabelle/Value.hs" = \<open>
@@ -1522,7 +1529,7 @@
         Text s -> Buffer.add s
 
 content_of :: Body -> Bytes
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
+content_of = Buffer.build_content . fold add_content
 
 
 {- string representation -}
@@ -1540,7 +1547,7 @@
 
 instance Show Tree where
   show tree =
-    Buffer.empty |> show_tree tree |> Buffer.content |> make_string
+    make_string $ Buffer.build_content (show_tree tree)
     where
       show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
@@ -1831,7 +1838,7 @@
 buffer (XML.Text s) = Buffer.add s
 
 string_of_body :: XML.Body -> Bytes
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
+string_of_body = Buffer.build_content . buffer_body
 
 string_of :: XML.Tree -> Bytes
 string_of = string_of_body . single
@@ -2049,7 +2056,7 @@
 formatted = YXML.string_of_body . symbolic
 
 unformatted :: T -> Bytes
-unformatted prt = Buffer.empty |> out prt |> Buffer.content
+unformatted = Buffer.build_content . out
   where
     out (Block markup _ _ prts) =
       let (bg, en) = YXML.output_markup markup