# HG changeset patch
# User wenzelm
# Date 1373452408 -7200
# Node ID 815461c835b9b49d2e77593130ec1c97b3272661
# Parent  2fb1f9cf80d3a2b5571f214445f2746b6c4497da
tuned start_execution: avoid sleep on worker thread;

diff -r 2fb1f9cf80d3 -r 815461c835b9 src/Pure/PIDE/document.ML
--- 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;
 
 
diff -r 2fb1f9cf80d3 -r 815461c835b9 src/Pure/PIDE/protocol.ML
--- 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 _ =