more scalable on 32-bit Poly/ML;
authorwenzelm
Wed Feb 27 17:33:39 2019 +0100 (3 months ago ago)
changeset 70026d28e8199dcb9
parent 70025 b21ddfa7042b
child 70027 e02e3763e7a4
more scalable on 32-bit Poly/ML;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/yxml.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Wed Feb 27 16:28:46 2019 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 17:33:39 2019 +0100
     1.3 @@ -117,10 +117,10 @@
     1.4  
     1.5              val _ =
     1.6                Output.protocol_message Markup.assign_update
     1.7 -                [(new_id, assign_update) |>
     1.8 +                ((new_id, assign_update) |>
     1.9                    let open XML.Encode
    1.10                    in pair int (list (pair int (list int))) end
    1.11 -                  |> YXML.string_of_body];
    1.12 +                  |> YXML.chunks_of_body);
    1.13            in Document.start_execution state' end)));
    1.14  
    1.15  val _ =
     2.1 --- a/src/Pure/PIDE/yxml.ML	Wed Feb 27 16:28:46 2019 +0100
     2.2 +++ b/src/Pure/PIDE/yxml.ML	Wed Feb 27 17:33:39 2019 +0100
     2.3 @@ -23,6 +23,7 @@
     2.4    val output_markup: Markup.T -> string * string
     2.5    val buffer_body: XML.body -> Buffer.T -> Buffer.T
     2.6    val buffer: XML.tree -> Buffer.T -> Buffer.T
     2.7 +  val chunks_of_body: XML.body -> string list
     2.8    val string_of_body: XML.body -> string
     2.9    val string_of: XML.tree -> string
    2.10    val output_markup_elem: Markup.T -> (string * string) * string
    2.11 @@ -78,6 +79,7 @@
    2.12        Buffer.add XYX
    2.13    | buffer (XML.Text s) = Buffer.add s
    2.14  
    2.15 +fun chunks_of_body body = Buffer.empty |> buffer_body body |> Buffer.chunks;
    2.16  fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
    2.17  val string_of = string_of_body o single;
    2.18