improved interleaving of start_execution vs. cancel_execution of the next update;

--- 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;