# HG changeset patch
# User wenzelm
# Date 1279711514 -7200
# Node ID 3a6ec95a9f68764525653793a31b1013e01b97d0
# Parent  814b1bca7f35501efc0da3b925bb89ba518db12f
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

diff -r 814b1bca7f35 -r 3a6ec95a9f68 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Jul 20 23:16:21 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Jul 21 13:25:14 2010 +0200
@@ -36,6 +36,7 @@
   val is_worker: unit -> bool
   val worker_task: unit -> Task_Queue.task option
   val worker_group: unit -> Task_Queue.group option
+  val worker_subgroup: unit -> Task_Queue.group
   type 'a future
   val task_of: 'a future -> task
   val group_of: 'a future -> group
@@ -83,8 +84,7 @@
 val is_worker = is_some o thread_data;
 val worker_task = Option.map #1 o thread_data;
 val worker_group = Option.map #2 o thread_data;
-
-fun new_group () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = Task_Queue.new_group (worker_group ());
 
 
 (* datatype future *)
@@ -388,7 +388,7 @@
   let
     val group =
       (case opt_group of
-        NONE => new_group ()
+        NONE => worker_subgroup ()
       | SOME group => group);
     val (result, job) = future_job group e;
     val task = SYNCHRONIZED "enqueue" (fn () =>
@@ -490,7 +490,7 @@
       Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
   in Future {promised = true, task = task, group = group, result = result} end;
 
-fun promise () = promise_group (new_group ());
+fun promise () = promise_group (worker_subgroup ());
 
 fun fulfill_result (Future {promised, task, group, result}) res =
   let
diff -r 814b1bca7f35 -r 3a6ec95a9f68 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Jul 20 23:16:21 2010 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Jul 21 13:25:14 2010 +0200
@@ -28,8 +28,8 @@
 
 fun raw_map f xs =
   if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
-    let val group = Task_Queue.new_group (Future.worker_group ())
-    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
+    let val shared_group = Task_Queue.new_group (Future.worker_group ())
+    in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end
   else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);
diff -r 814b1bca7f35 -r 3a6ec95a9f68 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 23:16:21 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Jul 21 13:25:14 2010 +0200
@@ -567,8 +567,7 @@
 fun async_state (tr as Transition {print, ...}) st =
   if print then
     ignore
-      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
-        (fn () =>
+      (Future.fork (fn () =>
           setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
   else ();