more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
(* Title: Pure/System/message_channel.ML
Author: Makarius
Preferably asynchronous channel for Isabelle messages.
*)
signature MESSAGE_CHANNEL =
sig
type message
val message: string -> Properties.T -> string -> message
type T
val send: T -> message -> unit
val shutdown: T -> unit
val make: System_Channel.T -> T
end;
structure Message_Channel: MESSAGE_CHANNEL =
struct
(* message *)
datatype message = Message of string list;
fun chunk s = [string_of_int (size s), "\n", s];
fun message name raw_props body =
let
val robust_props = map (pairself YXML.embed_controls) raw_props;
val header = YXML.string_of (XML.Elem ((name, robust_props), []));
in Message (chunk header @ chunk body) end;
fun output_message channel (Message ss) =
List.app (System_Channel.output channel) ss;
(* flush *)
fun flush channel = ignore (try System_Channel.flush channel);
val flush_message = message Markup.protocolN Markup.flush "";
fun flush_output channel = (output_message channel flush_message; flush channel);
(* channel *)
datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
fun send (Message_Channel {send, ...}) = send;
fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
fun message_output mbox channel =
let
fun loop receive =
(case receive mbox of
SOME NONE => flush_output channel
| SOME (SOME msg) =>
(output_message channel msg;
loop (Mailbox.receive_timeout (seconds 0.02)))
| NONE => (flush_output channel; loop (SOME o Mailbox.receive)));
in fn () => loop (SOME o Mailbox.receive) end;
fun make channel =
if Multithreading.available then
let
val mbox = Mailbox.create ();
val thread = Simple_Thread.fork false (message_output mbox channel);
fun send msg = Mailbox.send mbox (SOME msg);
fun shutdown () =
(Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
in Message_Channel {send = send, shutdown = shutdown} end
else
let
fun send msg = (output_message channel msg; flush channel);
in Message_Channel {send = send, shutdown = fn () => ()} end;
end;