# HG changeset patch
# User wenzelm
# Date 1526821545 -7200
# Node ID 326f4bcc5abc6c0393e6635c69c23f25da39f659
# Parent  b95a43d8b826f623182d2aa0ffb3583bd37a0714
more scalable;

diff -r b95a43d8b826 -r 326f4bcc5abc src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Sun May 20 15:05:17 2018 +0200
+++ b/src/Pure/General/buffer.ML	Sun May 20 15:05:45 2018 +0200
@@ -11,6 +11,7 @@
   val add: string -> T -> T
   val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
+  val chunks: T -> string list
   val output: T -> BinIO.outstream -> unit
 end;
 
@@ -30,7 +31,33 @@
 
 fun content (Buffer xs) = implode (rev xs);
 
-fun output (Buffer xs) stream =
-  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (rev xs);
+
+(* chunks *)
+
+local
+
+val max_chunk = 4096;
+
+fun add_chunk [] res = res
+  | add_chunk chunk res = implode chunk :: res;
+
+fun rev_chunks [] _ chunk res = add_chunk chunk res
+  | rev_chunks (x :: xs) len chunk res =
+      let
+        val n = size x;
+        val len' = len + n;
+      in
+        if len' < max_chunk then rev_chunks xs len' (x :: chunk) res
+        else rev_chunks xs n [x] (add_chunk chunk res)
+      end;
+
+in
+
+fun chunks (Buffer xs) = rev_chunks xs 0 [] [];
+
+fun output buf stream =
+  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
 
 end;
+
+end;
diff -r b95a43d8b826 -r 326f4bcc5abc src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sun May 20 15:05:17 2018 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sun May 20 15:05:45 2018 +0200
@@ -21,6 +21,8 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
+  val buffer_body: XML.body -> Buffer.T -> Buffer.T
+  val buffer: XML.tree -> Buffer.T -> Buffer.T
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val output_markup_elem: Markup.T -> (string * string) * string
@@ -66,17 +68,17 @@
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
-fun string_of_body body =
-  let
-    fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
-    fun tree (XML.Elem ((name, atts), ts)) =
-          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
-          trees ts #>
-          Buffer.add XYX
-      | tree (XML.Text s) = Buffer.add s
-    and trees ts = fold tree ts;
-  in Buffer.empty |> trees body |> Buffer.content end;
+fun buffer_attrib (a, x) =
+  Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
 
+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
+
+fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
 val string_of = string_of_body o single;