# HG changeset patch
# User wenzelm
# Date 1334956606 -7200
# Node ID e5c5e73f3e30a3fce5d4928b159fcfa7f2398b20
# Parent  50f9f699b2d769df6859f96e537900d0bea1a191
improved interleaving of start_execution vs. cancel_execution of the next update;

diff -r 50f9f699b2d7 -r e5c5e73f3e30 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Apr 20 23:15:44 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 20 23:16:46 2012 +0200
@@ -314,20 +314,25 @@
       in () end;
 
     val (version_id, group, running) = execution_of state;
+
     val _ =
-      nodes_of (the_version state version_id) |> Graph.schedule
-        (fn deps => fn (name, node) =>
-          if not (visible_node node) andalso finished_theory node then
-            Future.value ()
-          else
-            (singleton o Future.forks)
-              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
-                deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
-              (fn () =>
-                iterate_entries (fn ((_, id), opt_exec) => fn () =>
-                  (case opt_exec of
-                    SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
-                  | NONE => NONE)) node ()));
+      (singleton o Future.forks)
+        {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
+        (fn () =>
+         (OS.Process.sleep (seconds 0.02);
+          nodes_of (the_version state version_id) |> Graph.schedule
+            (fn deps => fn (name, node) =>
+              if not (visible_node node) andalso finished_theory node then
+                Future.value ()
+              else
+                (singleton o Future.forks)
+                  {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
+                    deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
+                  (fn () =>
+                    iterate_entries (fn ((_, id), opt_exec) => fn () =>
+                      (case opt_exec of
+                        SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+                      | NONE => NONE)) node ()))));
   in () end;