# HG changeset patch # User wenzelm # Date 1375201156 -7200 # Node ID 9d3c9862d1dddedac29ec0d94c2b56871a42fe44 # Parent 0d6f2a87d1a58618557cc6b06b22ff6296443131 recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive; diff -r 0d6f2a87d1a5 -r 9d3c9862d1dd etc/options --- 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)" diff -r 0d6f2a87d1a5 -r 9d3c9862d1dd src/Pure/Concurrent/event_timer.ML --- 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; diff -r 0d6f2a87d1a5 -r 9d3c9862d1dd src/Pure/PIDE/document.ML --- 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)); diff -r 0d6f2a87d1a5 -r 9d3c9862d1dd src/Pure/ROOT.ML --- 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 ()