106 |
106 |
107 |
107 |
108 |
108 |
109 (** interrupts **) |
109 (** interrupts **) |
110 |
110 |
|
111 exception Interrupt; |
|
112 |
111 local |
113 local |
112 |
114 |
113 datatype 'a result = |
115 fun capture f x = ((f x): unit; NONE) handle exn => SOME exn; |
114 Result of 'a | |
|
115 Exn of exn; |
|
116 |
116 |
117 fun capture f x = Result (f x) handle exn => Exn exn; |
117 fun release NONE = () |
118 |
118 | release (SOME exn) = raise exn; |
119 fun release (Result x) = x |
|
120 | release (Exn exn) = raise exn; |
|
121 |
|
122 |
|
123 val sig_int = Signals.sigINT; |
|
124 val sig_int_mask = Signals.MASK [Signals.sigINT]; |
|
125 |
|
126 fun interruptible () = |
|
127 (case Signals.masked () of |
|
128 Signals.MASKALL => false |
|
129 | Signals.MASK sigs => List.all (fn s => s <> sig_int) sigs); |
|
130 |
|
131 val mask_signals = Signals.maskSignals; |
|
132 val unmask_signals = Signals.unmaskSignals; |
|
133 |
|
134 fun change_mask ok change unchange f x = |
|
135 if ok () then f x |
|
136 else |
|
137 let |
|
138 val _ = change sig_int_mask; |
|
139 val result = capture f x; |
|
140 val _ = unchange sig_int_mask; |
|
141 in release result end; |
|
142 |
119 |
143 in |
120 in |
144 |
121 |
|
122 fun ignore_interrupt f x = |
|
123 let |
|
124 val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE); |
|
125 val result = capture f x; |
|
126 val _ = Signals.setHandler (Signals.sigINT, old_handler); |
|
127 in release result end; |
145 |
128 |
146 (* mask / unmask interrupt *) |
129 fun raise_interrupt f x = |
147 |
|
148 fun mask_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f; |
|
149 fun unmask_interrupt f = change_mask interruptible unmask_signals mask_signals f; |
|
150 |
|
151 |
|
152 (* exhibit interrupt (via exception) *) |
|
153 |
|
154 exception Interrupt; |
|
155 |
|
156 fun exhibit_interrupt f x = |
|
157 let |
130 let |
158 val orig_handler = Signals.inqHandler sig_int; |
|
159 fun reset_handler () = (Signals.setHandler (sig_int, orig_handler); ()); |
|
160 |
|
161 val interrupted = ref false; |
131 val interrupted = ref false; |
162 |
132 val result = ref NONE; |
163 fun set_handler cont = |
133 val old_handler = Signals.inqHandler Signals.sigINT; |
164 Signals.setHandler (sig_int, Signals.HANDLER (fn _ => (interrupted := true; cont))); |
|
165 |
|
166 fun proceed cont = |
|
167 let |
|
168 val _ = set_handler cont; |
|
169 val result = unmask_interrupt (capture f) x; |
|
170 val _ = reset_handler (); |
|
171 in release result end; |
|
172 in |
134 in |
173 SMLofNJ.Cont.callcc proceed; |
135 SMLofNJ.Cont.callcc (fn cont => |
174 reset_handler (); |
136 (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont))); |
175 if ! interrupted then raise Interrupt else () |
137 result := capture f x)); |
176 end; |
138 Signals.setHandler (Signals.sigINT, old_handler); |
|
139 if ! interrupted then raise Interrupt else release (! result) |
|
140 end; |
177 |
141 |
178 end; |
142 end; |
179 |
143 |
180 |
144 |
181 |
145 |