src/Pure/PIDE/document.ML
changeset 52810 cd28423ba19f
parent 52808 143f225e50f5
child 52849 199e9fa5a5c2
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 31 12:31:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 31 12:46:53 2013 +0200
     1.3 @@ -306,7 +306,6 @@
     1.4        val {version_id, execution_id, delay_request, frontier} = execution;
     1.5  
     1.6        val delay = seconds (Options.default_real "editor_execution_delay");
     1.7 -      val pri = Options.default_int "editor_execution_priority";
     1.8  
     1.9        val _ = Future.cancel delay_request;
    1.10        val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    1.11 @@ -331,7 +330,7 @@
    1.12                    (singleton o Future.forks)
    1.13                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.14                        deps = more_deps @ map #2 (maps #2 deps),
    1.15 -                      pri = pri, interrupts = false} body;
    1.16 +                      pri = 0, interrupts = false} body;
    1.17                in [(name, Future.task_of future)] end
    1.18              else []);
    1.19        val frontier' = (fold o fold) Symtab.update new_tasks frontier;