equal
deleted
inserted
replaced
56 val fork_pri: int -> (unit -> 'a) -> 'a future |
56 val fork_pri: int -> (unit -> 'a) -> 'a future |
57 val fork: (unit -> 'a) -> 'a future |
57 val fork: (unit -> 'a) -> 'a future |
58 val join_results: 'a future list -> 'a Exn.result list |
58 val join_results: 'a future list -> 'a Exn.result list |
59 val join_result: 'a future -> 'a Exn.result |
59 val join_result: 'a future -> 'a Exn.result |
60 val join: 'a future -> 'a |
60 val join: 'a future -> 'a |
|
61 val value_result: 'a Exn.result -> 'a future |
61 val value: 'a -> 'a future |
62 val value: 'a -> 'a future |
62 val map: ('a -> 'b) -> 'a future -> 'b future |
63 val map: ('a -> 'b) -> 'a future -> 'b future |
63 val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list |
64 val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list |
64 val promise_group: Task_Queue.group -> 'a future |
65 val promise_group: Task_Queue.group -> 'a future |
65 val promise: unit -> 'a future |
66 val promise: unit -> 'a future |
522 fun join x = Exn.release (join_result x); |
523 fun join x = Exn.release (join_result x); |
523 |
524 |
524 |
525 |
525 (* fast-path versions -- bypassing task queue *) |
526 (* fast-path versions -- bypassing task queue *) |
526 |
527 |
527 fun value (x: 'a) = |
528 fun value_result (res: 'a Exn.result) = |
528 let |
529 let |
529 val task = Task_Queue.dummy_task (); |
530 val task = Task_Queue.dummy_task (); |
530 val group = Task_Queue.group_of_task task; |
531 val group = Task_Queue.group_of_task task; |
531 val result = Single_Assignment.var "value" : 'a result; |
532 val result = Single_Assignment.var "value" : 'a result; |
532 val _ = assign_result group result (Exn.Res x); |
533 val _ = assign_result group result res; |
533 in Future {promised = false, task = task, result = result} end; |
534 in Future {promised = false, task = task, result = result} end; |
|
535 |
|
536 fun value x = value_result (Exn.Res x); |
534 |
537 |
535 fun map_future f x = |
538 fun map_future f x = |
536 let |
539 let |
537 val task = task_of x; |
540 val task = task_of x; |
538 val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task)); |
541 val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task)); |
551 (fn () => f (join x)) |
554 (fn () => f (join x)) |
552 end; |
555 end; |
553 |
556 |
554 fun cond_forks args es = |
557 fun cond_forks args es = |
555 if Multithreading.enabled () then forks args es |
558 if Multithreading.enabled () then forks args es |
556 else map (fn e => value (e ())) es; |
559 else map (fn e => value_result (Exn.interruptible_capture e ())) es; |
557 |
560 |
558 |
561 |
559 (* promised futures -- fulfilled by external means *) |
562 (* promised futures -- fulfilled by external means *) |
560 |
563 |
561 fun promise_group group : 'a future = |
564 fun promise_group group : 'a future = |