author | wenzelm |
Tue, 13 Apr 2021 11:44:47 +0200 | |
changeset 73577 | 6c8fc3c038eb |
parent 73564 | a021bb558feb |
child 73578 | 629868f96c81 |
permissions | -rw-r--r-- |
52584 | 1 |
(* Title: Pure/System/message_channel.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Preferably asynchronous channel for Isabelle messages. |
|
5 |
*) |
|
6 |
||
7 |
signature MESSAGE_CHANNEL = |
|
8 |
sig |
|
9 |
type T |
|
73577 | 10 |
val send_message: T -> string -> Properties.T -> XML.body list -> unit |
52584 | 11 |
val shutdown: T -> unit |
69449 | 12 |
val make: BinIO.outstream -> T |
52584 | 13 |
end; |
14 |
||
15 |
structure Message_Channel: MESSAGE_CHANNEL = |
|
16 |
struct |
|
17 |
||
73577 | 18 |
datatype message = Message of XML.body list; |
19 |
datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; |
|
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52584
diff
changeset
|
20 |
|
73577 | 21 |
fun send_message (Message_Channel {send, ...}) name raw_props chunks = |
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52584
diff
changeset
|
22 |
let |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58857
diff
changeset
|
23 |
val robust_props = map (apply2 YXML.embed_controls) raw_props; |
73559 | 24 |
val header = [XML.Elem ((name, robust_props), [])]; |
73577 | 25 |
in send (Message (header :: chunks)) end; |
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52584
diff
changeset
|
26 |
|
52584 | 27 |
fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); |
28 |
||
69449 | 29 |
fun message_output mbox stream = |
52584 | 30 |
let |
73564
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
31 |
fun continue () = Mailbox.receive NONE mbox |> received |
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
32 |
and received [] = continue () |
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
33 |
| received (NONE :: _) = () |
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
34 |
| received (SOME (Message chunks) :: rest) = |
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
35 |
(Byte_Message.write_message_yxml stream chunks; received rest); |
a021bb558feb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm
parents:
73559
diff
changeset
|
36 |
in continue end; |
52584 | 37 |
|
69449 | 38 |
fun make stream = |
62359 | 39 |
let |
40 |
val mbox = Mailbox.create (); |
|
41 |
val thread = |
|
71692 | 42 |
Isabelle_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false} |
69449 | 43 |
(message_output mbox stream); |
62359 | 44 |
fun send msg = Mailbox.send mbox (SOME msg); |
45 |
fun shutdown () = |
|
71692 | 46 |
(Mailbox.send mbox NONE; Mailbox.await_empty mbox; Isabelle_Thread.join thread); |
62359 | 47 |
in Message_Channel {send = send, shutdown = shutdown} end; |
52584 | 48 |
|
49 |
end; |