# HG changeset patch
# User wenzelm
# Date 1334083337 -7200
# Node ID c486ac962b8999ce3ebe0a3e56a14e25f7db29b5
# Parent  b2eafae4d40109acb221924b2f8e7b92d492a172
tuned future priorities: print 0, goal ~1, execute ~2;

diff -r b2eafae4d401 -r c486ac962b89 src/Pure/PIDE/document.ML
--- 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
diff -r b2eafae4d401 -r c486ac962b89 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Apr 10 16:50:30 2012 +0200
+++ b/src/Pure/goal.ML	Tue Apr 10 20:42:17 2012 +0200
@@ -125,7 +125,7 @@
       val _ = forked 1;
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = 0, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));