simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
authorwenzelm
Wed Jul 31 12:46:53 2013 +0200 (2013-07-31)
changeset 52810cd28423ba19f
parent 52809 e750169a5884
child 52811 dae6c61f991e
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
etc/options
src/Pure/PIDE/document.ML
     1.1 --- a/etc/options	Wed Jul 31 12:31:10 2013 +0200
     1.2 +++ b/etc/options	Wed Jul 31 12:46:53 2013 +0200
     1.3 @@ -129,9 +129,6 @@
     1.4  option editor_execution_delay : real = 0.02
     1.5    -- "delay for start of execution process after document update (seconds)"
     1.6  
     1.7 -option editor_execution_priority : int = -1
     1.8 -  -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.9 -
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12  
     2.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 31 12:31:10 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 31 12:46:53 2013 +0200
     2.3 @@ -306,7 +306,6 @@
     2.4        val {version_id, execution_id, delay_request, frontier} = execution;
     2.5  
     2.6        val delay = seconds (Options.default_real "editor_execution_delay");
     2.7 -      val pri = Options.default_int "editor_execution_priority";
     2.8  
     2.9        val _ = Future.cancel delay_request;
    2.10        val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    2.11 @@ -331,7 +330,7 @@
    2.12                    (singleton o Future.forks)
    2.13                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.14                        deps = more_deps @ map #2 (maps #2 deps),
    2.15 -                      pri = pri, interrupts = false} body;
    2.16 +                      pri = 0, interrupts = false} body;
    2.17                in [(name, Future.task_of future)] end
    2.18              else []);
    2.19        val frontier' = (fold o fold) Symtab.update new_tasks frontier;