src/Pure/PIDE/document.ML

         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if visible_node node orelse pending_result node then
               let
                 val former_task = Symtab.lookup frontier name;
+                fun body () =
+                  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 ()
+                  handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
                 val future =
                   (singleton o Future.forks)
                     {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
                       deps = the_list former_task @ map #2 (maps #2 deps),
-                      pri = pri, interrupts = false}
-                    (fn () =>
-                      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 ());
+                      pri = pri, interrupts = false} body;
               in [(name, Future.task_of future)] end
             else [])
       else [];
     val frontier' = (fold o fold) Symtab.update new_tasks frontier;
     val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};