--- a/src/Pure/PIDE/document.ML Sun Jun 03 20:37:16 2018 +0200
+++ b/src/Pure/PIDE/document.ML Sun Jun 03 22:02:20 2018 +0200
@@ -314,17 +314,20 @@
type execution =
{version_id: Document_ID.version, (*static version id*)
execution_id: Document_ID.execution, (*dynamic execution id*)
- delay_request: unit future}; (*pending event timer request*)
+ delay_request: unit future, (*pending event timer request*)
+ parallel_prints: Command.exec list}; (*parallel prints for early execution*)
val no_execution: execution =
{version_id = Document_ID.none,
execution_id = Document_ID.none,
- delay_request = Future.value ()};
+ delay_request = Future.value (),
+ parallel_prints = []};
-fun new_execution version_id delay_request : execution =
+fun new_execution version_id delay_request parallel_prints : execution =
{version_id = version_id,
execution_id = Execution.start (),
- delay_request = delay_request};
+ delay_request = delay_request,
+ parallel_prints = parallel_prints};
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
@@ -347,12 +350,23 @@
(* document versions *)
-fun define_version version_id version =
+fun parallel_prints_node node =
+ iterate_entries (fn (_, opt_exec) => fn rev_result =>
+ (case opt_exec of
+ SOME (eval, prints) =>
+ (case filter Command.parallel_print prints of
+ [] => SOME rev_result
+ | prints' => SOME ((eval, prints') :: rev_result))
+ | NONE => NONE)) node [] |> rev;
+
+fun define_version version_id version assigned_nodes =
map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
let
- val versions' = Inttab.update_new (version_id, version) versions
+ val version' = fold put_node assigned_nodes version;
+ val versions' = Inttab.update_new (version_id, version') versions
handle Inttab.DUP dup => err_dup "document version" dup;
- val execution' = new_execution version_id delay_request;
+ val parallel_prints = maps (parallel_prints_node o #2) assigned_nodes;
+ val execution' = new_execution version_id delay_request parallel_prints;
in (versions', blobs, commands, execution') end);
fun the_version (State {versions, ...}) version_id =
@@ -479,12 +493,16 @@
fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
timeit "Document.start_execution" (fn () =>
let
- val {version_id, execution_id, delay_request} = execution;
+ val {version_id, execution_id, delay_request, parallel_prints} = execution;
val delay = seconds (Options.default_real "editor_execution_delay");
val _ = Future.cancel delay_request;
val delay_request' = Event_Timer.future (Time.now () + delay);
+ val delay = Future.task_of delay_request';
+
+ val parallel_prints' = parallel_prints
+ |> map_filter (Command.exec_parallel_prints execution_id [delay]);
fun finished_import (name, (node, _)) =
finished_result node orelse is_some (Thy_Info.lookup_theory name);
@@ -516,14 +534,13 @@
(singleton o Future.forks)
{name = "theory:" ^ name,
group = SOME (Future.new_group NONE),
- deps =
- Future.task_of delay_request' :: Execution.active_tasks name @
- maps (the_list o #2 o #2) deps,
+ deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
pri = 0, interrupts = false} body;
in (node, SOME (Future.task_of future)) end
else (node, NONE));
val execution' =
- {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
+ {version_id = version_id, execution_id = execution_id,
+ delay_request = delay_request', parallel_prints = parallel_prints'};
in (versions, blobs, commands, execution') end));
@@ -838,7 +855,7 @@
val assigned_nodes = map_filter #3 updated;
val state' = state
- |> define_version new_version_id (fold put_node assigned_nodes new_version);
+ |> define_version new_version_id new_version assigned_nodes;
in (removed, assign_result, state') end);