tuned start_execution: avoid sleep on worker thread;

--- a/src/Pure/PIDE/document.ML	Wed Jul 10 12:10:32 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 10 12:33:28 2013 +0200
@@ -313,23 +313,21 @@
   let
     val {version_id, group, running} = execution_of state;
     val _ =
-      (singleton o Future.forks)
-        {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
-        (fn () =>
-         (OS.Process.sleep (seconds 0.02);
-          nodes_of (the_version state version_id) |> String_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 (_, opt_exec) => fn () =>
-                      (case opt_exec of
-                        SOME exec => if ! running then SOME (Command.execute exec) else NONE
-                      | NONE => NONE)) node ()))));
+      if not (! running) orelse Task_Queue.is_canceled group then []
+      else
+        nodes_of (the_version state version_id) |> String_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 (_, opt_exec) => fn () =>
+                    (case opt_exec of
+                      SOME exec => if ! running then SOME (Command.execute exec) else NONE
+                    | NONE => NONE)) node ()));
   in () end;
 
 

--- a/src/Pure/PIDE/protocol.ML	Wed Jul 10 12:10:32 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Jul 10 12:33:28 2013 +0200
@@ -58,7 +58,9 @@
 
         val _ = List.app Future.cancel_group (Goal.reset_futures ());
         val _ = Isabelle_Process.reset_tracing ();
-        val _ = Document.start_execution state';
+        val _ =
+          Event_Timer.request (Time.now () + seconds 0.02)
+            (fn () => Document.start_execution state');
       in state' end));
 
 val _ =