# HG changeset patch
# User wenzelm
# Date 1374330475 -7200
# Node ID 8979d830950b8bffc643ed090c4519b2f5e25374
# Parent  a4e4802753b91848a29ca33e15c33f886357781a
option editor_execution_priority;

diff -r a4e4802753b9 -r 8979d830950b etc/options
--- 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"
 
diff -r a4e4802753b9 -r 8979d830950b src/Pure/PIDE/document.ML
--- 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