src/Pure/PIDE/document.ML
changeset 52573 815461c835b9
parent 52570 26d84a0b9209
child 52586 7a0935571a23
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 10 12:10:32 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 10 12:33:28 2013 +0200
     1.3 @@ -313,23 +313,21 @@
     1.4    let
     1.5      val {version_id, group, running} = execution_of state;
     1.6      val _ =
     1.7 -      (singleton o Future.forks)
     1.8 -        {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
     1.9 -        (fn () =>
    1.10 -         (OS.Process.sleep (seconds 0.02);
    1.11 -          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.12 -            (fn deps => fn (name, node) =>
    1.13 -              if not (visible_node node) andalso finished_theory node then
    1.14 -                Future.value ()
    1.15 -              else
    1.16 -                (singleton o Future.forks)
    1.17 -                  {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.18 -                    deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    1.19 -                  (fn () =>
    1.20 -                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.21 -                      (case opt_exec of
    1.22 -                        SOME exec => if ! running then SOME (Command.execute exec) else NONE
    1.23 -                      | NONE => NONE)) node ()))));
    1.24 +      if not (! running) orelse Task_Queue.is_canceled group then []
    1.25 +      else
    1.26 +        nodes_of (the_version state version_id) |> String_Graph.schedule
    1.27 +          (fn deps => fn (name, node) =>
    1.28 +            if not (visible_node node) andalso finished_theory node then
    1.29 +              Future.value ()
    1.30 +            else
    1.31 +              (singleton o Future.forks)
    1.32 +                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.33 +                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    1.34 +                (fn () =>
    1.35 +                  iterate_entries (fn (_, opt_exec) => fn () =>
    1.36 +                    (case opt_exec of
    1.37 +                      SOME exec => if ! running then SOME (Command.execute exec) else NONE
    1.38 +                    | NONE => NONE)) node ()));
    1.39    in () end;
    1.40  
    1.41