equal
deleted
inserted
replaced
44 type task = Task_Queue.task |
44 type task = Task_Queue.task |
45 type group = Task_Queue.group |
45 type group = Task_Queue.group |
46 val new_group: group option -> group |
46 val new_group: group option -> group |
47 val worker_task: unit -> task option |
47 val worker_task: unit -> task option |
48 val worker_group: unit -> group option |
48 val worker_group: unit -> group option |
|
49 val the_worker_group: unit -> group |
49 val worker_subgroup: unit -> group |
50 val worker_subgroup: unit -> group |
50 val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b |
51 val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b |
51 type 'a future |
52 type 'a future |
52 val task_of: 'a future -> task |
53 val task_of: 'a future -> task |
53 val peek: 'a future -> 'a Exn.result option |
54 val peek: 'a future -> 'a Exn.result option |
97 fun worker_task () = the_default NONE (Thread.getLocal tag); |
98 fun worker_task () = the_default NONE (Thread.getLocal tag); |
98 fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x; |
99 fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x; |
99 end; |
100 end; |
100 |
101 |
101 val worker_group = Option.map Task_Queue.group_of_task o worker_task; |
102 val worker_group = Option.map Task_Queue.group_of_task o worker_task; |
|
103 |
|
104 fun the_worker_group () = |
|
105 (case worker_group () of |
|
106 SOME group => group |
|
107 | NONE => raise Fail "Missing worker thread context"); |
|
108 |
102 fun worker_subgroup () = new_group (worker_group ()); |
109 fun worker_subgroup () = new_group (worker_group ()); |
103 |
110 |
104 fun worker_guest name group f x = |
111 fun worker_guest name group f x = |
105 if is_some (worker_task ()) then |
112 if is_some (worker_task ()) then |
106 raise Fail "Already running as worker thread" |
113 raise Fail "Already running as worker thread" |
554 fun join_results xs = |
561 fun join_results xs = |
555 let |
562 let |
556 val _ = |
563 val _ = |
557 if forall is_finished xs then () |
564 if forall is_finished xs then () |
558 else if Multithreading.self_critical () then |
565 else if Multithreading.self_critical () then |
559 error "Cannot join future values within critical section" |
566 raise Fail "Cannot join future values within critical section" |
560 else if is_some (worker_task ()) then join_work (map task_of xs) |
567 else if is_some (worker_task ()) then join_work (map task_of xs) |
561 else List.app (ignore o Single_Assignment.await o result_of) xs; |
568 else List.app (ignore o Single_Assignment.await o result_of) xs; |
562 in map get_result xs end; |
569 in map get_result xs end; |
563 |
570 |
564 end; |
571 end; |