# HG changeset patch
# User wenzelm
# Date 1314199008 -7200
# Node ID 364fd07398f51214d58d29b71762be48dde7aa35
# Parent  33a5616a757186fa209092c847f92ede9e47e362
tuned pri: prefer purging of canceled execution;

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 =