minor performance tuning: avoid many small strings, notably in File_Stream.output;

--- a/src/Pure/PIDE/xml.ML	Fri Aug 30 17:00:21 2024 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Aug 31 16:00:16 2024 +0200
@@ -73,7 +73,23 @@
 
 open Output_Primitives.XML;
 
-val blob = map Text;
+val blob =
+  let
+    val limit = 8000;
+
+    val buffer = fn "" => I | s => cons s;
+    val output1 = fn "" => I | s => cons (Text s);
+    val output = fn [] => I | ss => cons (Text (implode ss));
+
+    fun make [] _ buf result = output buf result
+      | make (x :: xs) m buf result =
+          let val l = size x in
+            if l + m < limit then make xs (l + m) (buffer x buf) result
+            else if l + m = limit then make xs 0 [] (output (buffer x buf) result)
+            else if l >= limit then make xs 0 [] (output1 x (output buf result))
+            else make xs l [x] (output buf result)
+          end;
+  in fn xs => make (rev xs) 0 [] [] end
 
 fun is_empty (Text "") = true
   | is_empty _ = false;