src/Pure/PIDE/document.ML
changeset 52715 8979d830950b
parent 52655 3b2b1ef13979
child 52716 ecb46f11c366
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Jul 20 16:18:17 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Jul 20 16:27:55 2013 +0200
     1.3 @@ -297,6 +297,7 @@
     1.4  fun start_execution state =
     1.5    let
     1.6      val {version_id, execution_id} = execution_of state;
     1.7 +    val pri = Options.default_int "editor_execution_priority";
     1.8      val _ =
     1.9        if Execution.is_running execution_id then
    1.10          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.11 @@ -306,7 +307,7 @@
    1.12              else
    1.13                (singleton o Future.forks)
    1.14                  {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.15 -                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    1.16 +                  deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
    1.17                  (fn () =>
    1.18                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.19                      (case opt_exec of