10 signature EVENT_TIMER = |
10 signature EVENT_TIMER = |
11 sig |
11 sig |
12 eqtype request |
12 eqtype request |
13 val request: Time.time -> (unit -> unit) -> request |
13 val request: Time.time -> (unit -> unit) -> request |
14 val cancel: request -> bool |
14 val cancel: request -> bool |
|
15 val future: Time.time -> unit future |
15 val shutdown: unit -> unit |
16 val shutdown: unit -> unit |
16 val future: Time.time -> unit future |
|
17 end; |
17 end; |
18 |
18 |
19 structure Event_Timer: EVENT_TIMER = |
19 structure Event_Timer: EVENT_TIMER = |
20 struct |
20 struct |
21 |
21 |
97 val state' = make_state (requests', status, manager); |
97 val state' = make_state (requests', status, manager); |
98 in SOME (true, state') end |
98 in SOME (true, state') end |
99 | NONE => |
99 | NONE => |
100 if is_shutdown_req st |
100 if is_shutdown_req st |
101 then SOME (false, shutdown_ack_state) |
101 then SOME (false, shutdown_ack_state) |
102 else NONE)) = SOME false |
102 else NONE)) <> SOME false |
103 then () else manager_loop (); |
103 then manager_loop () else (); |
104 |
104 |
105 fun manager_check manager = |
105 fun manager_check manager = |
106 if is_some manager andalso Thread.isActive (the manager) then manager |
106 if is_some manager andalso Thread.isActive (the manager) then manager |
107 else SOME (Simple_Thread.fork false manager_loop); |
107 else SOME (Simple_Thread.fork false manager_loop); |
108 |
|
109 |
|
110 (* main operations *) |
|
111 |
|
112 fun request time event = |
|
113 Synchronized.change_result state (fn State {requests, status, manager} => |
|
114 let |
|
115 val req = new_request (); |
|
116 val requests' = add_request time (req, event) requests; |
|
117 val manager' = manager_check manager; |
|
118 in (req, make_state (requests', status, manager')) end); |
|
119 |
|
120 fun cancel req = |
|
121 Synchronized.change_result state (fn State {requests, status, manager} => |
|
122 let |
|
123 val (canceled, requests') = del_request req requests; |
|
124 val manager' = manager_check manager; |
|
125 in (canceled, make_state (requests', status, manager')) end); |
|
126 |
108 |
127 fun shutdown () = |
109 fun shutdown () = |
128 uninterruptible (fn restore_attributes => fn () => |
110 uninterruptible (fn restore_attributes => fn () => |
129 if Synchronized.change_result state (fn st as State {requests, status, manager} => |
111 if Synchronized.change_result state (fn st as State {requests, status, manager} => |
130 if is_shutdown Normal st then (false, st) |
112 if is_shutdown Normal st then (false, st) |
141 make_state (requests, Normal, manager)) |
123 make_state (requests, Normal, manager)) |
142 else () |
124 else () |
143 else ()) (); |
125 else ()) (); |
144 |
126 |
145 |
127 |
146 (* future *) |
128 (* main operations *) |
|
129 |
|
130 fun request time event = |
|
131 Synchronized.change_result state (fn State {requests, status, manager} => |
|
132 let |
|
133 val req = new_request (); |
|
134 val requests' = add_request time (req, event) requests; |
|
135 val manager' = manager_check manager; |
|
136 in (req, make_state (requests', status, manager')) end); |
|
137 |
|
138 fun cancel req = |
|
139 Synchronized.change_result state (fn State {requests, status, manager} => |
|
140 let |
|
141 val (canceled, requests') = del_request req requests; |
|
142 val manager' = manager_check manager; |
|
143 in (canceled, make_state (requests', status, manager')) end); |
147 |
144 |
148 val future = uninterruptible (fn _ => fn time => |
145 val future = uninterruptible (fn _ => fn time => |
149 let |
146 let |
150 val req: request Single_Assignment.var = Single_Assignment.var "request"; |
147 val req: request Single_Assignment.var = Single_Assignment.var "request"; |
151 fun abort () = ignore (cancel (Single_Assignment.await req)); |
148 fun abort () = ignore (cancel (Single_Assignment.await req)); |