equal
deleted
inserted
replaced
203 (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); |
203 (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); |
204 |
204 |
205 val channel = System_Channel.rendezvous socket; |
205 val channel = System_Channel.rendezvous socket; |
206 val msg_channel = init_channels channel; |
206 val msg_channel = init_channels channel; |
207 val _ = loop channel; |
207 val _ = loop channel; |
208 in Message_Channel.shutdown msg_channel end); |
208 val _ = Message_Channel.shutdown msg_channel; |
|
209 val _ = Private_Output.init_channels (); |
|
210 in () end); |
209 |
211 |
210 |
212 |
211 (* init options *) |
213 (* init options *) |
212 |
214 |
213 fun init_options () = |
215 fun init_options () = |