1.1 --- a/src/Pure/PIDE/document.ML	Tue Apr 10 16:50:30 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Apr 10 20:42:17 2012 +0200
     1.3 @@ -312,7 +312,7 @@
     1.4              else
     1.5                (singleton o Future.forks)
     1.6                  {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
     1.7 -                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
     1.8 +                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
     1.9                  (fn () =>
    1.10                    iterate_entries (fn ((_, id), opt_exec) => fn () =>
    1.11                      (case opt_exec of

     2.1 --- a/src/Pure/goal.ML	Tue Apr 10 16:50:30 2012 +0200
     2.2 +++ b/src/Pure/goal.ML	Tue Apr 10 20:42:17 2012 +0200
     2.3 @@ -125,7 +125,7 @@
     2.4        val _ = forked 1;
     2.5        val future =
     2.6          (singleton o Future.forks)
     2.7 -          {name = name, group = NONE, deps = [], pri = 0, interrupts = false}
     2.8 +          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
     2.9            (fn () =>
    2.10              Exn.release
    2.11                (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));