document update at high priority -- important;

--- a/src/Pure/PIDE/document.ML	Sat Jul 20 16:27:55 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Jul 20 16:29:06 2013 +0200
@@ -463,7 +463,7 @@
         (fn deps => fn (name, node) =>
           (singleton o Future.forks)
             {name = "Document.update", group = NONE,
-              deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+              deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
             (fn () =>
               let
                 val imports = map (apsnd Future.join) deps;