changeset 52716 | ecb46f11c366 |
parent 52715 | 8979d830950b |
child 52761 | 909167fdd367 |
1.1 --- a/src/Pure/PIDE/document.ML Sat Jul 20 16:27:55 2013 +0200 1.2 +++ b/src/Pure/PIDE/document.ML Sat Jul 20 16:29:06 2013 +0200 1.3 @@ -463,7 +463,7 @@ 1.4 (fn deps => fn (name, node) => 1.5 (singleton o Future.forks) 1.6 {name = "Document.update", group = NONE, 1.7 - deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} 1.8 + deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} 1.9 (fn () => 1.10 let 1.11 val imports = map (apsnd Future.join) deps;