--- a/src/Pure/PIDE/protocol.ML Thu May 31 22:10:06 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu May 31 22:27:13 2018 +0200
@@ -64,10 +64,6 @@
end);
val _ =
- Isabelle_Process.protocol_command "Document.consolidate_execution"
- (fn [] => Document.consolidate_execution (Document.state ()));
-
-val _ =
Isabelle_Process.protocol_command "Document.discontinue_execution"
(fn [] => Execution.discontinue ());
@@ -78,49 +74,52 @@
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] => Document.change_state (fn state =>
- let
- val _ = Execution.discontinue ();
+ (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] =>
+ 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 edits =
+ YXML.parse_body edits_yxml |>
+ let open XML.Decode in
+ list (pair string
+ (variant
+ [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+ fn ([], a) =>
+ let
+ val (master, (name, (imports, (keywords, errors)))) =
+ pair string (pair string (pair (list string)
+ (pair (list (pair string
+ (pair (pair string (list string)) (list string))))
+ (list YXML.string_of_body)))) a;
+ val imports' = map (rpair Position.none) imports;
+ val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+ val header = Thy_Header.make (name, Position.none) imports' keywords';
+ 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 = Value.parse_bool consolidate_string;
- val old_id = Document_ID.parse old_id_string;
- val new_id = Document_ID.parse new_id_string;
- val edits =
- YXML.parse_body edits_yxml |>
- let open XML.Decode in
- list (pair string
- (variant
- [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
- fn ([], a) =>
- let
- val (master, (name, (imports, (keywords, errors)))) =
- pair string (pair string (pair (list string)
- (pair (list (pair string
- (pair (pair string (list string)) (list string))))
- (list YXML.string_of_body)))) a;
- val imports' = map (rpair Position.none) imports;
- val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
- val header = Thy_Header.make (name, Position.none) imports' keywords';
- 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 _ = Execution.discontinue ();
- val (removed, assign_update, state') = Document.update old_id new_id edits state;
- val _ =
- (singleton o Future.forks)
- {name = "Document.update/remove", group = NONE,
- deps = Execution.snapshot removed,
- pri = Task_Queue.urgent_pri + 2, interrupts = false}
- (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
+ val (removed, assign_update, state') =
+ Document.update old_id new_id edits consolidate state;
+ val _ =
+ (singleton o Future.forks)
+ {name = "Document.update/remove", group = NONE,
+ deps = Execution.snapshot removed,
+ pri = Task_Queue.urgent_pri + 2, interrupts = false}
+ (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
- val _ =
- Output.protocol_message Markup.assign_update
- [(new_id, assign_update) |>
- let open XML.Encode
- in pair int (list (pair int (list int))) end
- |> YXML.string_of_body];
- in Document.start_execution state' end)));
+ val _ =
+ Output.protocol_message Markup.assign_update
+ [(new_id, assign_update) |>
+ let open XML.Encode
+ in pair int (list (pair int (list int))) end
+ |> YXML.string_of_body];
+ in Document.start_execution state' end)));
val _ =
Isabelle_Process.protocol_command "Document.remove_versions"