option editor_execution_priority;
authorwenzelm
Sat Jul 20 16:27:55 2013 +0200 (2013-07-20 ago)
changeset 527158979d830950b
parent 52714 a4e4802753b9
child 52716 ecb46f11c366
option editor_execution_priority;
etc/options
src/Pure/PIDE/document.ML
     1.1 --- a/etc/options	Sat Jul 20 16:18:17 2013 +0200
     1.2 +++ b/etc/options	Sat Jul 20 16:27:55 2013 +0200
     1.3 @@ -123,6 +123,9 @@
     1.4  public option editor_chart_delay : real = 3.0
     1.5    -- "delay for chart repainting"
     1.6  
     1.7 +public option editor_execution_priority : int = -2
     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	Sat Jul 20 16:18:17 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Jul 20 16:27:55 2013 +0200
     2.3 @@ -297,6 +297,7 @@
     2.4  fun start_execution state =
     2.5    let
     2.6      val {version_id, execution_id} = execution_of state;
     2.7 +    val pri = Options.default_int "editor_execution_priority";
     2.8      val _ =
     2.9        if Execution.is_running execution_id then
    2.10          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.11 @@ -306,7 +307,7 @@
    2.12              else
    2.13                (singleton o Future.forks)
    2.14                  {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.15 -                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    2.16 +                  deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
    2.17                  (fn () =>
    2.18                    iterate_entries (fn (_, opt_exec) => fn () =>
    2.19                      (case opt_exec of