32 |
32 |
33 fun output_message channel (Message ss) = |
33 fun output_message channel (Message ss) = |
34 List.app (System_Channel.output channel) ss; |
34 List.app (System_Channel.output channel) ss; |
35 |
35 |
36 |
36 |
37 (* flush *) |
|
38 |
|
39 fun flush channel = ignore (try System_Channel.flush channel); |
|
40 |
|
41 val flush_message = message Markup.protocolN Markup.flush []; |
|
42 fun flush_output channel = (output_message channel flush_message; flush channel); |
|
43 |
|
44 |
|
45 (* channel *) |
37 (* channel *) |
46 |
38 |
47 datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; |
39 datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; |
48 |
40 |
49 fun send (Message_Channel {send, ...}) = send; |
41 fun send (Message_Channel {send, ...}) = send; |
50 fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); |
42 fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); |
51 |
43 |
|
44 fun flush channel = ignore (try System_Channel.flush channel); |
|
45 |
52 fun message_output mbox channel = |
46 fun message_output mbox channel = |
53 let |
47 let |
54 fun loop receive = |
48 fun loop receive = |
55 (case receive mbox of |
49 (case receive mbox of |
56 SOME NONE => flush_output channel |
50 SOME NONE => flush channel |
57 | SOME (SOME msg) => |
51 | SOME (SOME msg) => |
58 (output_message channel msg; |
52 (output_message channel msg; |
59 loop (Mailbox.receive_timeout (seconds 0.02))) |
53 loop (Mailbox.receive_timeout (seconds 0.02))) |
60 | NONE => (flush_output channel; loop (SOME o Mailbox.receive))); |
54 | NONE => (flush channel; loop (SOME o Mailbox.receive))); |
61 in fn () => loop (SOME o Mailbox.receive) end; |
55 in fn () => loop (SOME o Mailbox.receive) end; |
62 |
56 |
63 fun make channel = |
57 fun make channel = |
64 if Multithreading.available then |
58 if Multithreading.available then |
65 let |
59 let |