--- a/src/Pure/PIDE/protocol.ML Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML Tue Jun 05 16:12:26 2018 +0200
@@ -74,7 +74,7 @@
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_string] =>
+ (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
Document.change_state (fn state =>
let
val old_id = Document_ID.parse old_id_string;
@@ -100,7 +100,9 @@
Document.Perspective (bool_atom a, map int_atom b,
list (pair int (pair string (list string))) c)]))
end;
- val consolidate = Value.parse_bool consolidate_string;
+ val consolidate =
+ YXML.parse_body consolidate_yxml |>
+ let open XML.Decode in list string end;
val _ = Execution.discontinue ();