recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
authorwenzelm
Tue Jul 30 18:19:16 2013 +0200 (2013-07-30)
changeset 527989d3c9862d1dd
parent 52797 0d6f2a87d1a5
child 52799 6a4498b048b7
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
etc/options
src/Pure/Concurrent/event_timer.ML
src/Pure/PIDE/document.ML
src/Pure/ROOT.ML
     1.1 --- a/etc/options	Tue Jul 30 16:22:07 2013 +0200
     1.2 +++ b/etc/options	Tue Jul 30 18:19:16 2013 +0200
     1.3 @@ -123,6 +123,9 @@
     1.4  public option editor_chart_delay : real = 3.0
     1.5    -- "delay for chart repainting"
     1.6  
     1.7 +option editor_execution_delay : real = 0.02
     1.8 +  -- "delay for start of execution process after document update (seconds)"
     1.9 +
    1.10  option editor_execution_priority : int = -1
    1.11    -- "execution priority of main document structure (e.g. 0, -1, -2)"
    1.12  
     2.1 --- a/src/Pure/Concurrent/event_timer.ML	Tue Jul 30 16:22:07 2013 +0200
     2.2 +++ b/src/Pure/Concurrent/event_timer.ML	Tue Jul 30 18:19:16 2013 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val request: Time.time -> event -> request
     2.5    val cancel: request -> bool
     2.6    val shutdown: unit -> unit
     2.7 +  val future: Time.time -> unit future
     2.8  end;
     2.9  
    2.10  structure Event_Timer: EVENT_TIMER =
    2.11 @@ -125,5 +126,16 @@
    2.12      else if is_none manager then SOME ((), init_state)
    2.13      else NONE);
    2.14  
    2.15 +
    2.16 +(* future *)
    2.17 +
    2.18 +val future = uninterruptible (fn _ => fn time =>
    2.19 +  let
    2.20 +    val req: request Single_Assignment.var = Single_Assignment.var "request";
    2.21 +    fun abort () = ignore (cancel (Single_Assignment.await req));
    2.22 +    val promise: unit future = Future.promise abort;
    2.23 +    val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
    2.24 +  in promise end);
    2.25 +
    2.26  end;
    2.27  
     3.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 30 16:22:07 2013 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 30 18:19:16 2013 +0200
     3.3 @@ -204,13 +204,16 @@
     3.4  type execution =
     3.5   {version_id: Document_ID.version,  (*static version id*)
     3.6    execution_id: Document_ID.execution,  (*dynamic execution id*)
     3.7 +  delay_request: unit future,  (*pending event timer request*)
     3.8    frontier: Future.task Symtab.table};  (*node name -> running execution task*)
     3.9  
    3.10  val no_execution: execution =
    3.11 -  {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
    3.12 +  {version_id = Document_ID.none, execution_id = Document_ID.none,
    3.13 +   delay_request = Future.value (), frontier = Symtab.empty};
    3.14  
    3.15 -fun new_execution version_id frontier : execution =
    3.16 -  {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
    3.17 +fun new_execution version_id delay_request frontier : execution =
    3.18 +  {version_id = version_id, execution_id = Execution.start (),
    3.19 +   delay_request = delay_request, frontier = frontier};
    3.20  
    3.21  abstype state = State of
    3.22   {versions: version Inttab.table,  (*version id -> document content*)
    3.23 @@ -231,11 +234,11 @@
    3.24  (* document versions *)
    3.25  
    3.26  fun define_version version_id version =
    3.27 -  map_state (fn (versions, commands, {frontier, ...}) =>
    3.28 +  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
    3.29      let
    3.30        val versions' = Inttab.update_new (version_id, version) versions
    3.31          handle Inttab.DUP dup => err_dup "document version" dup;
    3.32 -      val execution' = new_execution version_id frontier;
    3.33 +      val execution' = new_execution version_id delay_request frontier;
    3.34      in (versions', commands, execution') end);
    3.35  
    3.36  fun the_version (State {versions, ...}) version_id =
    3.37 @@ -299,15 +302,21 @@
    3.38  fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
    3.39    timeit "Document.start_execution" (fn () =>
    3.40      let
    3.41 -      val {version_id, execution_id, frontier} = execution;
    3.42 +      val {version_id, execution_id, delay_request, frontier} = execution;
    3.43 +
    3.44 +      val delay = seconds (Options.default_real "editor_execution_delay");
    3.45        val pri = Options.default_int "editor_execution_priority";
    3.46  
    3.47 +      val _ = Future.cancel delay_request;
    3.48 +      val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    3.49 +
    3.50        val new_tasks =
    3.51          nodes_of (the_version state version_id) |> String_Graph.schedule
    3.52            (fn deps => fn (name, node) =>
    3.53              if visible_node node orelse pending_result node then
    3.54                let
    3.55 -                val former_task = Symtab.lookup frontier name;
    3.56 +                val more_deps =
    3.57 +                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
    3.58                  fun body () =
    3.59                    iterate_entries (fn (_, opt_exec) => fn () =>
    3.60                      (case opt_exec of
    3.61 @@ -320,12 +329,14 @@
    3.62                  val future =
    3.63                    (singleton o Future.forks)
    3.64                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    3.65 -                      deps = the_list former_task @ map #2 (maps #2 deps),
    3.66 +                      deps = more_deps @ map #2 (maps #2 deps),
    3.67                        pri = pri, interrupts = false} body;
    3.68                in [(name, Future.task_of future)] end
    3.69              else []);
    3.70        val frontier' = (fold o fold) Symtab.update new_tasks frontier;
    3.71 -      val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
    3.72 +      val execution' =
    3.73 +        {version_id = version_id, execution_id = execution_id,
    3.74 +         delay_request = delay_request', frontier = frontier'};
    3.75      in (versions, commands, execution') end));
    3.76  
    3.77  
     4.1 --- a/src/Pure/ROOT.ML	Tue Jul 30 16:22:07 2013 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Tue Jul 30 18:19:16 2013 +0200
     4.3 @@ -70,8 +70,6 @@
     4.4  
     4.5  (* concurrency within the ML runtime *)
     4.6  
     4.7 -use "Concurrent/event_timer.ML";
     4.8 -
     4.9  if ML_System.is_polyml
    4.10  then use "ML/exn_properties_polyml.ML"
    4.11  else use "ML/exn_properties_dummy.ML";
    4.12 @@ -84,8 +82,6 @@
    4.13  if Multithreading.available then ()
    4.14  else use "Concurrent/single_assignment_sequential.ML";
    4.15  
    4.16 -if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    4.17 -
    4.18  if Multithreading.available
    4.19  then use "Concurrent/bash.ML"
    4.20  else use "Concurrent/bash_sequential.ML";
    4.21 @@ -93,6 +89,9 @@
    4.22  use "Concurrent/par_exn.ML";
    4.23  use "Concurrent/task_queue.ML";
    4.24  use "Concurrent/future.ML";
    4.25 +use "Concurrent/event_timer.ML";
    4.26 +
    4.27 +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    4.28  
    4.29  use "Concurrent/lazy.ML";
    4.30  if Multithreading.available then ()