recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

--- a/etc/options	Tue Jul 30 16:22:07 2013 +0200
+++ b/etc/options	Tue Jul 30 18:19:16 2013 +0200
@@ -123,6 +123,9 @@
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
+option editor_execution_delay : real = 0.02
+  -- "delay for start of execution process after document update (seconds)"
+
 option editor_execution_priority : int = -1
   -- "execution priority of main document structure (e.g. 0, -1, -2)"
 

--- a/src/Pure/Concurrent/event_timer.ML	Tue Jul 30 16:22:07 2013 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Tue Jul 30 18:19:16 2013 +0200
@@ -14,6 +14,7 @@
   val request: Time.time -> event -> request
   val cancel: request -> bool
   val shutdown: unit -> unit
+  val future: Time.time -> unit future
 end;
 
 structure Event_Timer: EVENT_TIMER =
@@ -125,5 +126,16 @@
     else if is_none manager then SOME ((), init_state)
     else NONE);
 
+
+(* future *)
+
+val future = uninterruptible (fn _ => fn time =>
+  let
+    val req: request Single_Assignment.var = Single_Assignment.var "request";
+    fun abort () = ignore (cancel (Single_Assignment.await req));
+    val promise: unit future = Future.promise abort;
+    val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
+  in promise end);
+
 end;
 

--- a/src/Pure/PIDE/document.ML	Tue Jul 30 16:22:07 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jul 30 18:19:16 2013 +0200
@@ -204,13 +204,16 @@
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
   execution_id: Document_ID.execution,  (*dynamic execution id*)
+  delay_request: unit future,  (*pending event timer request*)
   frontier: Future.task Symtab.table};  (*node name -> running execution task*)
 
 val no_execution: execution =
-  {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
+  {version_id = Document_ID.none, execution_id = Document_ID.none,
+   delay_request = Future.value (), frontier = Symtab.empty};
 
-fun new_execution version_id frontier : execution =
-  {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
+fun new_execution version_id delay_request frontier : execution =
+  {version_id = version_id, execution_id = Execution.start (),
+   delay_request = delay_request, frontier = frontier};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
@@ -231,11 +234,11 @@
 (* document versions *)
 
 fun define_version version_id version =
-  map_state (fn (versions, commands, {frontier, ...}) =>
+  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = new_execution version_id frontier;
+      val execution' = new_execution version_id delay_request frontier;
     in (versions', commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
@@ -299,15 +302,21 @@
 fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
-      val {version_id, execution_id, frontier} = execution;
+      val {version_id, execution_id, delay_request, frontier} = execution;
+
+      val delay = seconds (Options.default_real "editor_execution_delay");
       val pri = Options.default_int "editor_execution_priority";
 
+      val _ = Future.cancel delay_request;
+      val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
+
       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
               let
-                val former_task = Symtab.lookup frontier name;
+                val more_deps =
+                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
                 fun body () =
                   iterate_entries (fn (_, opt_exec) => fn () =>
                     (case opt_exec of
@@ -320,12 +329,14 @@
                 val future =
                   (singleton o Future.forks)
                     {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
-                      deps = the_list former_task @ map #2 (maps #2 deps),
+                      deps = more_deps @ map #2 (maps #2 deps),
                       pri = pri, interrupts = false} body;
               in [(name, Future.task_of future)] end
             else []);
       val frontier' = (fold o fold) Symtab.update new_tasks frontier;
-      val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
+      val execution' =
+        {version_id = version_id, execution_id = execution_id,
+         delay_request = delay_request', frontier = frontier'};
     in (versions, commands, execution') end));
 
 

--- a/src/Pure/ROOT.ML	Tue Jul 30 16:22:07 2013 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 30 18:19:16 2013 +0200
@@ -70,8 +70,6 @@
 
 (* concurrency within the ML runtime *)
 
-use "Concurrent/event_timer.ML";
-
 if ML_System.is_polyml
 then use "ML/exn_properties_polyml.ML"
 else use "ML/exn_properties_dummy.ML";
@@ -84,8 +82,6 @@
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
-
 if Multithreading.available
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
@@ -93,6 +89,9 @@
 use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
+use "Concurrent/event_timer.ML";
+
+if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
 
 use "Concurrent/lazy.ML";
 if Multithreading.available then ()