src/Pure/System/message_channel.ML
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52584 5cad4a5f5615
child 52800 1baa5d19ac44
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     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
    10   val send: T -> string list -> bool -> unit
    11   val shutdown: T -> unit
    12   val make: System_Channel.T -> T
    13 end;
    14 
    15 structure Message_Channel: MESSAGE_CHANNEL =
    16 struct
    17 
    18 datatype T = Message_Channel of
    19  {send: string list -> bool -> unit,
    20   shutdown: unit -> unit};
    21 
    22 fun send (Message_Channel {send, ...}) = send;
    23 fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
    24 
    25 fun flush channel = ignore (try System_Channel.flush channel);
    26 
    27 fun message_output mbox channel =
    28   let
    29     fun loop receive =
    30       (case receive mbox of
    31         SOME NONE => flush channel
    32       | SOME (SOME (msg, do_flush)) =>
    33          (List.app (fn s => System_Channel.output channel s) msg;
    34           if do_flush then flush channel else ();
    35           loop (Mailbox.receive_timeout (seconds 0.02)))
    36       | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    37   in fn () => loop (SOME o Mailbox.receive) end;
    38 
    39 fun make channel =
    40   if Multithreading.available then
    41     let
    42       val mbox = Mailbox.create ();
    43       val thread = Simple_Thread.fork false (message_output mbox channel);
    44       fun send msg do_flush = Mailbox.send mbox (SOME (msg, do_flush));
    45       fun shutdown () =
    46         (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
    47     in Message_Channel {send = send, shutdown = shutdown} end
    48   else
    49     let
    50       fun send msg = (List.app (fn s => System_Channel.output channel s) msg; flush channel);
    51     in Message_Channel {send = fn msg => fn _ => send msg, shutdown = fn () => ()} end;
    52 
    53 end;
    54