# HG changeset patch
# User wenzelm
# Date 1535801924 -7200
# Node ID d4681a748873c6a40df4f68d023a11253ac9ac84
# Parent  dd44e31ca2c639b0915695c88020c14f044a73d8
tuned;

diff -r dd44e31ca2c6 -r d4681a748873 src/Pure/PIDE/document.ML
--- 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' =