improved interleaving of start_execution vs. cancel_execution of the next update;
authorwenzelm
Fri Apr 20 23:16:46 2012 +0200 (2012-04-20 ago)
changeset 47633e5c5e73f3e30
parent 47632 50f9f699b2d7
child 47638 4923b8ba0f49
improved interleaving of start_execution vs. cancel_execution of the next update;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 20 23:15:44 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 20 23:16:46 2012 +0200
     1.3 @@ -314,20 +314,25 @@
     1.4        in () end;
     1.5  
     1.6      val (version_id, group, running) = execution_of state;
     1.7 +
     1.8      val _ =
     1.9 -      nodes_of (the_version state version_id) |> Graph.schedule
    1.10 -        (fn deps => fn (name, node) =>
    1.11 -          if not (visible_node node) andalso finished_theory node then
    1.12 -            Future.value ()
    1.13 -          else
    1.14 -            (singleton o Future.forks)
    1.15 -              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.16 -                deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    1.17 -              (fn () =>
    1.18 -                iterate_entries (fn ((_, id), opt_exec) => fn () =>
    1.19 -                  (case opt_exec of
    1.20 -                    SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
    1.21 -                  | NONE => NONE)) node ()));
    1.22 +      (singleton o Future.forks)
    1.23 +        {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
    1.24 +        (fn () =>
    1.25 +         (OS.Process.sleep (seconds 0.02);
    1.26 +          nodes_of (the_version state version_id) |> 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 ((_, id), opt_exec) => fn () =>
    1.36 +                      (case opt_exec of
    1.37 +                        SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
    1.38 +                      | NONE => NONE)) node ()))));
    1.39    in () end;
    1.40  
    1.41