--- a/etc/options Sat Jul 20 16:18:17 2013 +0200
+++ b/etc/options Sat Jul 20 16:27:55 2013 +0200
@@ -123,6 +123,9 @@
public option editor_chart_delay : real = 3.0
-- "delay for chart repainting"
+public option editor_execution_priority : int = -2
+ -- "execution priority of main document structure (e.g. 0, -1, -2)"
+
section "Miscellaneous Tools"
--- a/src/Pure/PIDE/document.ML Sat Jul 20 16:18:17 2013 +0200
+++ b/src/Pure/PIDE/document.ML Sat Jul 20 16:27:55 2013 +0200
@@ -297,6 +297,7 @@
fun start_execution state =
let
val {version_id, execution_id} = execution_of state;
+ val pri = Options.default_int "editor_execution_priority";
val _ =
if Execution.is_running execution_id then
nodes_of (the_version state version_id) |> String_Graph.schedule
@@ -306,7 +307,7 @@
else
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group NONE),
- deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
+ deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
(fn () =>
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of