clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
authorwenzelm
Wed Jul 21 13:25:14 2010 +0200 (2010-07-21 ago)
changeset 378653a6ec95a9f68
parent 37864 814b1bca7f35
child 37866 cd1d1bc7684c
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 20 23:16:21 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Jul 21 13:25:14 2010 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4    val is_worker: unit -> bool
     1.5    val worker_task: unit -> Task_Queue.task option
     1.6    val worker_group: unit -> Task_Queue.group option
     1.7 +  val worker_subgroup: unit -> Task_Queue.group
     1.8    type 'a future
     1.9    val task_of: 'a future -> task
    1.10    val group_of: 'a future -> group
    1.11 @@ -83,8 +84,7 @@
    1.12  val is_worker = is_some o thread_data;
    1.13  val worker_task = Option.map #1 o thread_data;
    1.14  val worker_group = Option.map #2 o thread_data;
    1.15 -
    1.16 -fun new_group () = Task_Queue.new_group (worker_group ());
    1.17 +fun worker_subgroup () = Task_Queue.new_group (worker_group ());
    1.18  
    1.19  
    1.20  (* datatype future *)
    1.21 @@ -388,7 +388,7 @@
    1.22    let
    1.23      val group =
    1.24        (case opt_group of
    1.25 -        NONE => new_group ()
    1.26 +        NONE => worker_subgroup ()
    1.27        | SOME group => group);
    1.28      val (result, job) = future_job group e;
    1.29      val task = SYNCHRONIZED "enqueue" (fn () =>
    1.30 @@ -490,7 +490,7 @@
    1.31        Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
    1.32    in Future {promised = true, task = task, group = group, result = result} end;
    1.33  
    1.34 -fun promise () = promise_group (new_group ());
    1.35 +fun promise () = promise_group (worker_subgroup ());
    1.36  
    1.37  fun fulfill_result (Future {promised, task, group, result}) res =
    1.38    let
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Jul 20 23:16:21 2010 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Jul 21 13:25:14 2010 +0200
     2.3 @@ -28,8 +28,8 @@
     2.4  
     2.5  fun raw_map f xs =
     2.6    if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
     2.7 -    let val group = Task_Queue.new_group (Future.worker_group ())
     2.8 -    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
     2.9 +    let val shared_group = Task_Queue.new_group (Future.worker_group ())
    2.10 +    in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end
    2.11    else map (Exn.capture f) xs;
    2.12  
    2.13  fun map f xs = Exn.release_first (raw_map f xs);
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 23:16:21 2010 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 21 13:25:14 2010 +0200
     3.3 @@ -567,8 +567,7 @@
     3.4  fun async_state (tr as Transition {print, ...}) st =
     3.5    if print then
     3.6      ignore
     3.7 -      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
     3.8 -        (fn () =>
     3.9 +      (Future.fork (fn () =>
    3.10            setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
    3.11    else ();
    3.12