tuned -- short-circuit result;
authorwenzelm
Tue Jun 05 14:15:49 2018 +0200 (13 months ago)
changeset 68380f249e1f5623b
parent 68379 1b0ce345d3c8
child 68381 2fd3a6d6ba2e
tuned -- short-circuit result;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jun 05 14:07:51 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jun 05 14:15:49 2018 +0200
     1.3 @@ -689,13 +689,16 @@
     1.4    (case finished_result_theory node of
     1.5      SOME (result_id, thy) =>
     1.6        let
     1.7 -        val eval_ids =
     1.8 -          iterate_entries (fn (_, opt_exec) => fn eval_ids =>
     1.9 -            (case opt_exec of
    1.10 -              SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    1.11 -            | NONE => NONE)) node [];
    1.12 +        val active_tasks =
    1.13 +          (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
    1.14 +            if active then NONE
    1.15 +            else
    1.16 +              (case opt_exec of
    1.17 +                NONE => NONE
    1.18 +              | SOME (eval, _) =>
    1.19 +                  SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
    1.20        in
    1.21 -        if null (Execution.snapshot eval_ids) then
    1.22 +        if not active_tasks then
    1.23            let
    1.24              val consolidation =
    1.25                if Options.bool options "editor_presentation" then