equal
deleted
inserted
replaced
68 val join: 'a future -> 'a |
68 val join: 'a future -> 'a |
69 val value_result: 'a Exn.result -> 'a future |
69 val value_result: 'a Exn.result -> 'a future |
70 val value: 'a -> 'a future |
70 val value: 'a -> 'a future |
71 val cond_forks: params -> (unit -> 'a) list -> 'a future list |
71 val cond_forks: params -> (unit -> 'a) list -> 'a future list |
72 val map: ('a -> 'b) -> 'a future -> 'b future |
72 val map: ('a -> 'b) -> 'a future -> 'b future |
73 val flat: 'a list future list -> 'a list future |
|
74 val promise_group: group -> (unit -> unit) -> 'a future |
73 val promise_group: group -> (unit -> unit) -> 'a future |
75 val promise: (unit -> unit) -> 'a future |
74 val promise: (unit -> unit) -> 'a future |
76 val fulfill_result: 'a future -> 'a Exn.result -> unit |
75 val fulfill_result: 'a future -> 'a Exn.result -> unit |
77 val fulfill: 'a future -> 'a -> unit |
76 val fulfill: 'a future -> 'a -> unit |
78 val terminate: group -> unit |
77 val terminate: group -> unit |
605 (singleton o cond_forks) |
604 (singleton o cond_forks) |
606 {name = "map_future", group = SOME group, deps = [task], |
605 {name = "map_future", group = SOME group, deps = [task], |
607 pri = Task_Queue.pri_of_task task, interrupts = true} |
606 pri = Task_Queue.pri_of_task task, interrupts = true} |
608 (fn () => f (join x)) |
607 (fn () => f (join x)) |
609 end; |
608 end; |
610 |
|
611 fun flat_future futures = |
|
612 (case filter_out is_finished futures of |
|
613 [] => value_result (Exn.interruptible_capture (flat o joins) futures) |
|
614 | [x] => map_future (fn _ => flat (joins (futures))) x |
|
615 | xs => |
|
616 let |
|
617 val tasks = map task_of xs; |
|
618 val pri = foldl1 Int.min (map Task_Queue.pri_of_task tasks); |
|
619 in |
|
620 (singleton o cond_forks) |
|
621 {name = "flat_future", group = NONE, deps = tasks, pri = pri, interrupts = true} |
|
622 (fn () => flat (joins (futures))) |
|
623 end); |
|
624 |
609 |
625 |
610 |
626 (* promised futures -- fulfilled by external means *) |
611 (* promised futures -- fulfilled by external means *) |
627 |
612 |
628 fun promise_group group abort : 'a future = |
613 fun promise_group group abort : 'a future = |
703 wait scheduler_event)); |
688 wait scheduler_event)); |
704 |
689 |
705 |
690 |
706 (*final declarations of this structure!*) |
691 (*final declarations of this structure!*) |
707 val map = map_future; |
692 val map = map_future; |
708 val flat = flat_future; |
|
709 |
693 |
710 end; |
694 end; |
711 |
695 |
712 type 'a future = 'a Future.future; |
696 type 'a future = 'a Future.future; |
713 |
697 |