simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

--- a/etc/options	Wed Jul 31 12:31:10 2013 +0200
+++ b/etc/options	Wed Jul 31 12:46:53 2013 +0200
@@ -129,9 +129,6 @@
 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)"
-
 
 section "Miscellaneous Tools"
 

--- a/src/Pure/PIDE/document.ML	Wed Jul 31 12:31:10 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 31 12:46:53 2013 +0200
@@ -306,7 +306,6 @@
       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));
@@ -331,7 +330,7 @@
                   (singleton o Future.forks)
                     {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
                       deps = more_deps @ map #2 (maps #2 deps),
-                      pri = pri, interrupts = false} body;
+                      pri = 0, interrupts = false} body;
               in [(name, Future.task_of future)] end
             else []);
       val frontier' = (fold o fold) Symtab.update new_tasks frontier;