# HG changeset patch
# User wenzelm
# Date 1376072193 -7200
# Node ID 13687b130f1fb865741d94154286baff8e050fa1
# Parent  4b053d8d0e7e2ea8d6b27210e57e30adca907ab3
retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);

diff -r 4b053d8d0e7e -r 13687b130f1f src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Aug 09 20:01:50 2013 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 09 20:16:33 2013 +0200
@@ -35,9 +35,13 @@
   else
     uninterruptible (fn restore_attributes => fn () =>
       let
-        val group = Future.new_group (Future.worker_group ());
+        val (group, pri) =
+          (case Future.worker_task () of
+            SOME task =>
+              (Future.new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
+          | NONE => (Future.new_group NONE, 0));
         val futures =
-          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
+          Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
             (map (fn x => fn () => f x) xs);
         val results =
           restore_attributes Future.join_results futures