more timing;
tuned -- Execution.is_running always holds due to immediate start;

--- a/src/Pure/PIDE/document.ML	Tue Jul 30 15:45:01 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jul 30 16:01:19 2013 +0200
@@ -7,6 +7,7 @@
 
 signature DOCUMENT =
 sig
+  val timing: bool Unsynchronized.ref
   type node_header = string * Thy_Header.header * string list
   datatype node_edit =
     Clear |    (* FIXME unused !? *)
@@ -19,7 +20,6 @@
   val define_command: Document_ID.command -> string -> string -> state -> state
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
-  val timing: bool Unsynchronized.ref
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
     Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
@@ -29,6 +29,11 @@
 structure Document: DOCUMENT =
 struct
 
+val timing = Unsynchronized.ref false;
+fun timeit msg e = cond_timeit (! timing) msg e;
+
+
+
 (** document structure **)
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
@@ -292,12 +297,12 @@
 (* document execution *)
 
 fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
-  let
-    val {version_id, execution_id, frontier} = execution;
-    val pri = Options.default_int "editor_execution_priority";
+  timeit "Document.start_execution" (fn () =>
+    let
+      val {version_id, execution_id, frontier} = execution;
+      val pri = Options.default_int "editor_execution_priority";
 
-    val new_tasks =
-      if Execution.is_running execution_id then
+      val new_tasks =
         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if visible_node node orelse pending_result node then
@@ -318,11 +323,10 @@
                       deps = the_list former_task @ map #2 (maps #2 deps),
                       pri = pri, interrupts = false} body;
               in [(name, Future.task_of future)] end
-            else [])
-      else [];
-    val frontier' = (fold o fold) Symtab.update new_tasks frontier;
-    val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
-  in (versions, commands, execution') end);
+            else []);
+      val frontier' = (fold o fold) Symtab.update new_tasks frontier;
+      val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
+    in (versions, commands, execution') end));
 
 
 
@@ -346,9 +350,6 @@
 
 (* update *)
 
-val timing = Unsynchronized.ref false;
-fun timeit msg e = cond_timeit (! timing) msg e;
-
 local
 
 fun make_required nodes =