equal
deleted
inserted
replaced
66 |
66 |
67 fun chunk s = [string_of_int (size s), "\n", s]; |
67 fun chunk s = [string_of_int (size s), "\n", s]; |
68 |
68 |
69 fun message mbox ch raw_props body = |
69 fun message mbox ch raw_props body = |
70 let |
70 let |
71 val robust_props = map (pairself YXML.escape_controls) raw_props; |
71 val robust_props = map (pairself YXML.embed_controls) raw_props; |
72 val header = YXML.string_of (XML.Elem ((ch, robust_props), [])); |
72 val header = YXML.string_of (XML.Elem ((ch, robust_props), [])); |
73 in Mailbox.send mbox (chunk header @ chunk body) end; |
73 in Mailbox.send mbox (chunk header @ chunk body) end; |
74 |
74 |
75 fun standard_message mbox with_serial ch body = |
75 fun standard_message mbox with_serial ch body = |
76 if body = "" then () |
76 if body = "" then () |