# HG changeset patch
# User wenzelm
# Date 1528200949 -7200
# Node ID f249e1f5623b34b3421e3451017d9e71a755446f
# Parent  1b0ce345d3c846b515cf88305eb8fc49fbaa3fdc
tuned -- short-circuit result;

diff -r 1b0ce345d3c8 -r f249e1f5623b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Jun 05 14:07:51 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jun 05 14:15:49 2018 +0200
@@ -689,13 +689,16 @@
   (case finished_result_theory node of
     SOME (result_id, thy) =>
       let
-        val eval_ids =
-          iterate_entries (fn (_, opt_exec) => fn eval_ids =>
-            (case opt_exec of
-              SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
-            | NONE => NONE)) node [];
+        val active_tasks =
+          (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
+            if active then NONE
+            else
+              (case opt_exec of
+                NONE => NONE
+              | SOME (eval, _) =>
+                  SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
       in
-        if null (Execution.snapshot eval_ids) then
+        if not active_tasks then
           let
             val consolidation =
               if Options.bool options "editor_presentation" then