more scalable;
authorwenzelm
Sun May 20 15:05:45 2018 +0200 (21 months ago)
changeset 68228326f4bcc5abc
parent 68227 b95a43d8b826
child 68229 18c36ac0acaa
more scalable;
src/Pure/General/buffer.ML
src/Pure/PIDE/yxml.ML
     1.1 --- a/src/Pure/General/buffer.ML	Sun May 20 15:05:17 2018 +0200
     1.2 +++ b/src/Pure/General/buffer.ML	Sun May 20 15:05:45 2018 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val add: string -> T -> T
     1.5    val markup: Markup.T -> (T -> T) -> T -> T
     1.6    val content: T -> string
     1.7 +  val chunks: T -> string list
     1.8    val output: T -> BinIO.outstream -> unit
     1.9  end;
    1.10  
    1.11 @@ -30,7 +31,33 @@
    1.12  
    1.13  fun content (Buffer xs) = implode (rev xs);
    1.14  
    1.15 -fun output (Buffer xs) stream =
    1.16 -  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (rev xs);
    1.17 +
    1.18 +(* chunks *)
    1.19 +
    1.20 +local
    1.21 +
    1.22 +val max_chunk = 4096;
    1.23 +
    1.24 +fun add_chunk [] res = res
    1.25 +  | add_chunk chunk res = implode chunk :: res;
    1.26 +
    1.27 +fun rev_chunks [] _ chunk res = add_chunk chunk res
    1.28 +  | rev_chunks (x :: xs) len chunk res =
    1.29 +      let
    1.30 +        val n = size x;
    1.31 +        val len' = len + n;
    1.32 +      in
    1.33 +        if len' < max_chunk then rev_chunks xs len' (x :: chunk) res
    1.34 +        else rev_chunks xs n [x] (add_chunk chunk res)
    1.35 +      end;
    1.36 +
    1.37 +in
    1.38 +
    1.39 +fun chunks (Buffer xs) = rev_chunks xs 0 [] [];
    1.40 +
    1.41 +fun output buf stream =
    1.42 +  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
    1.43  
    1.44  end;
    1.45 +
    1.46 +end;
     2.1 --- a/src/Pure/PIDE/yxml.ML	Sun May 20 15:05:17 2018 +0200
     2.2 +++ b/src/Pure/PIDE/yxml.ML	Sun May 20 15:05:45 2018 +0200
     2.3 @@ -21,6 +21,8 @@
     2.4    val embed_controls: string -> string
     2.5    val detect: string -> bool
     2.6    val output_markup: Markup.T -> string * string
     2.7 +  val buffer_body: XML.body -> Buffer.T -> Buffer.T
     2.8 +  val buffer: XML.tree -> Buffer.T -> Buffer.T
     2.9    val string_of_body: XML.body -> string
    2.10    val string_of: XML.tree -> string
    2.11    val output_markup_elem: Markup.T -> (string * string) * string
    2.12 @@ -66,17 +68,17 @@
    2.13    if Markup.is_empty markup then Markup.no_output
    2.14    else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    2.15  
    2.16 -fun string_of_body body =
    2.17 -  let
    2.18 -    fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
    2.19 -    fun tree (XML.Elem ((name, atts), ts)) =
    2.20 -          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
    2.21 -          trees ts #>
    2.22 -          Buffer.add XYX
    2.23 -      | tree (XML.Text s) = Buffer.add s
    2.24 -    and trees ts = fold tree ts;
    2.25 -  in Buffer.empty |> trees body |> Buffer.content end;
    2.26 +fun buffer_attrib (a, x) =
    2.27 +  Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
    2.28  
    2.29 +fun buffer_body ts = fold buffer ts
    2.30 +and buffer (XML.Elem ((name, atts), ts)) =
    2.31 +      Buffer.add XY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add X #>
    2.32 +      buffer_body ts #>
    2.33 +      Buffer.add XYX
    2.34 +  | buffer (XML.Text s) = Buffer.add s
    2.35 +
    2.36 +fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
    2.37  val string_of = string_of_body o single;
    2.38  
    2.39