diff -r 33a5616a7571 -r 364fd07398f5 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 24 17:14:31 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 17:16:48 2011 +0200
@@ -415,7 +415,7 @@
                 in
                   (singleton o Future.forks)
                     {name = "Document.edit", group = NONE,
-                      deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
+                      deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
                     (fn () =>
                       let
                         val prev_exec =