# HG changeset patch
# User wenzelm
# Date 1551386244 -3600
# Node ID 09f200c658ed2443828bb86c4132ff112492eead
# Parent  bf2cd27714fb4899f3a6f7a158c2aac1408e8824
more scalable on 32-bit Poly/ML;

diff -r bf2cd27714fb -r 09f200c658ed src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:16:17 2019 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:37:24 2019 +0100
@@ -74,15 +74,18 @@
 val _ =
   Isabelle_Process.protocol_command "Document.update"
     (Future.task_context "Document.update" (Future.new_group NONE)
-      (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
+      (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
         Document.change_state (fn state =>
           let
             val old_id = Document_ID.parse old_id_string;
             val new_id = Document_ID.parse new_id_string;
+            val consolidate =
+              YXML.parse_body consolidate_yxml |>
+                let open XML.Decode in list string end;
             val edits =
-              YXML.parse_body edits_yxml |>
+              edits_yxml |> map (YXML.parse_body #>
                 let open XML.Decode in
-                  list (pair string
+                  pair string
                     (variant
                      [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                       fn ([], a) =>
@@ -98,11 +101,8 @@
                         in Document.Deps {master = master, header = header, errors = errors} end,
                       fn (a :: b, c) =>
                         Document.Perspective (bool_atom a, map int_atom b,
-                          list (pair int (pair string (list string))) c)]))
-                end;
-            val consolidate =
-              YXML.parse_body consolidate_yxml |>
-                let open XML.Decode in list string end;
+                          list (pair int (pair string (list string))) c)])
+                end);
 
             val _ = Execution.discontinue ();
 
diff -r bf2cd27714fb -r 09f200c658ed src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Feb 28 21:16:17 2019 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Feb 28 21:37:24 2019 +0100
@@ -283,6 +283,11 @@
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
   {
+    val consolidate_yxml =
+    {
+      import XML.Encode._
+      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
+    }
     val edits_yxml =
     {
       import XML.Encode._
@@ -303,22 +308,11 @@
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
-      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
-      {
-        val (name, edit) = node_edit
-        pair(string, encode_edit(name))(name.node, edit)
-      })
-      Symbol.encode_yxml(encode_edits(edits))
+      edits.map({ case (name, edit) =>
+        Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
     }
-
-    val consolidate_yxml =
-    {
-      import XML.Encode._
-      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
-    }
-
-    protocol_command(
-      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml)
+    protocol_command("Document.update",
+      (Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml): _*)
   }
 
   def remove_versions(versions: List[Document.Version])