equal
deleted
inserted
replaced
12 val lazy: (unit -> 'a) -> 'a lazy |
12 val lazy: (unit -> 'a) -> 'a lazy |
13 val value: 'a -> 'a lazy |
13 val value: 'a -> 'a lazy |
14 val peek: 'a lazy -> 'a Exn.result option |
14 val peek: 'a lazy -> 'a Exn.result option |
15 val is_running: 'a lazy -> bool |
15 val is_running: 'a lazy -> bool |
16 val is_finished: 'a lazy -> bool |
16 val is_finished: 'a lazy -> bool |
17 val finished_result: 'a lazy -> 'a Exn.result option |
|
18 val force_result: 'a lazy -> 'a Exn.result |
17 val force_result: 'a lazy -> 'a Exn.result |
19 val force: 'a lazy -> 'a |
18 val force: 'a lazy -> 'a |
20 val map: ('a -> 'b) -> 'a lazy -> 'b lazy |
19 val map: ('a -> 'b) -> 'a lazy -> 'b lazy |
21 val future: Future.params -> 'a lazy -> 'a future |
20 val future: Future.params -> 'a lazy -> 'a future |
22 end; |
21 end; |
52 fun is_running x = is_future (not o Future.is_finished) x; |
51 fun is_running x = is_future (not o Future.is_finished) x; |
53 |
52 |
54 fun is_finished x = |
53 fun is_finished x = |
55 is_future (fn res => |
54 is_future (fn res => |
56 Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x; |
55 Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x; |
57 |
|
58 fun finished_result (Lazy var) = |
|
59 (case Synchronized.value var of |
|
60 Expr _ => NONE |
|
61 | Result res => |
|
62 if Future.is_finished res then |
|
63 let val result = Future.join_result res |
|
64 in if Exn.is_interrupt_exn result then NONE else SOME result end |
|
65 else NONE); |
|
66 |
56 |
67 |
57 |
68 (* force result *) |
58 (* force result *) |
69 |
59 |
70 fun force_result (Lazy var) = |
60 fun force_result (Lazy var) = |