--- 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 ();
--- 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])