# HG changeset patch
# User wenzelm
# Date 1375267613 -7200
# Node ID cd28423ba19fe25392f98133e4dfe3c109e507f7
# Parent  e750169a58848df71960178251d6dccdca9a86f5
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

diff -r e750169a5884 -r cd28423ba19f etc/options
--- 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"
 
diff -r e750169a5884 -r cd28423ba19f src/Pure/PIDE/document.ML
--- 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;