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));