changeset 47415 | c486ac962b89 |
parent 47407 | 8da23ecc70cd |
child 47420 | 0dbe6c69eda2 |
--- a/src/Pure/PIDE/document.ML Tue Apr 10 16:50:30 2012 +0200 +++ b/src/Pure/PIDE/document.ML Tue Apr 10 20:42:17 2012 +0200 @@ -312,7 +312,7 @@ else (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), - deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} + deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} (fn () => iterate_entries (fn ((_, id), opt_exec) => fn () => (case opt_exec of