--- a/src/Pure/PIDE/document.ML Fri Aug 31 22:25:58 2018 +0200
+++ b/src/Pure/PIDE/document.ML Sat Sep 01 13:38:44 2018 +0200
@@ -514,28 +514,28 @@
(fn deps => fn (name, node) =>
if Symtab.defined required name orelse visible_node node orelse pending_result node then
let
- fun body () =
- (Execution.worker_task_active true name;
- if forall finished_import deps then
- iterate_entries (fn (_, opt_exec) => fn () =>
- (case opt_exec of
- SOME exec =>
- if Execution.is_running execution_id
- then SOME (Command.exec execution_id exec)
- else NONE
- | NONE => NONE)) node ()
- else ();
- Execution.worker_task_active false name)
- handle exn =>
- (Output.system_message (Runtime.exn_message exn);
- Execution.worker_task_active false name;
- Exn.reraise exn);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,
group = SOME (Future.new_group NONE),
deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
- pri = 0, interrupts = false} body;
+ pri = 0, interrupts = false}
+ (fn () =>
+ (Execution.worker_task_active true name;
+ if forall finished_import deps then
+ iterate_entries (fn (_, opt_exec) => fn () =>
+ (case opt_exec of
+ SOME exec =>
+ if Execution.is_running execution_id
+ then SOME (Command.exec execution_id exec)
+ else NONE
+ | NONE => NONE)) node ()
+ else ();
+ Execution.worker_task_active false name)
+ handle exn =>
+ (Output.system_message (Runtime.exn_message exn);
+ Execution.worker_task_active false name;
+ Exn.reraise exn));
in (node, SOME (Future.task_of future)) end
else (node, NONE));
val execution' =