equal
deleted
inserted
replaced
29 val fork: (unit -> 'a) -> 'a future |
29 val fork: (unit -> 'a) -> 'a future |
30 val join_results: 'a future list -> 'a Exn.result list |
30 val join_results: 'a future list -> 'a Exn.result list |
31 val join_result: 'a future -> 'a Exn.result |
31 val join_result: 'a future -> 'a Exn.result |
32 val joins: 'a future list -> 'a list |
32 val joins: 'a future list -> 'a list |
33 val join: 'a future -> 'a |
33 val join: 'a future -> 'a |
|
34 val forked_results: {name: string, deps: Task_Queue.task list} -> |
|
35 (unit -> 'a) list -> 'a Exn.result list |
34 val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b |
36 val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b |
35 val value_result: 'a Exn.result -> 'a future |
37 val value_result: 'a Exn.result -> 'a future |
36 val value: 'a -> 'a future |
38 val value: 'a -> 'a future |
37 val cond_forks: params -> (unit -> 'a) list -> 'a future list |
39 val cond_forks: params -> (unit -> 'a) list -> 'a future list |
38 val map: ('a -> 'b) -> 'a future -> 'b future |
40 val map: ('a -> 'b) -> 'a future -> 'b future |
537 fun join_result x = singleton join_results x; |
539 fun join_result x = singleton join_results x; |
538 fun joins xs = Par_Exn.release_all (join_results xs); |
540 fun joins xs = Par_Exn.release_all (join_results xs); |
539 fun join x = Exn.release (join_result x); |
541 fun join x = Exn.release (join_result x); |
540 |
542 |
541 |
543 |
|
544 (* forked results: nested parallel evaluation *) |
|
545 |
|
546 fun forked_results {name, deps} es = |
|
547 Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
|
548 let |
|
549 val (group, pri) = |
|
550 (case worker_task () of |
|
551 SOME task => |
|
552 (new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task) |
|
553 | NONE => (new_group NONE, 0)); |
|
554 val futures = |
|
555 forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es; |
|
556 in |
|
557 restore_attributes join_results futures |
|
558 handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn) |
|
559 end) (); |
|
560 |
|
561 |
542 (* task context for running thread *) |
562 (* task context for running thread *) |
543 |
563 |
544 fun task_context name group f x = |
564 fun task_context name group f x = |
545 Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => |
565 Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => |
546 let |
566 let |