src/Pure/Concurrent/mailbox.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 29564 f8b933a62151
child 52583 0a7240d88e09
permissions -rw-r--r--
map_range (and map_index) combinator
     1 (*  Title:      Pure/Concurrent/mailbox.ML
     2     Author:     Makarius
     3 
     4 Message exchange via mailbox, with non-blocking send (due to unbounded
     5 queueing) and potentially blocking receive.
     6 *)
     7 
     8 signature MAILBOX =
     9 sig
    10   type 'a T
    11   val create: unit -> 'a T
    12   val send: 'a T -> 'a -> unit
    13   val receive: 'a T -> 'a
    14   val receive_timeout: Time.time -> 'a T -> 'a option
    15 end;
    16 
    17 structure Mailbox: MAILBOX =
    18 struct
    19 
    20 datatype 'a T = Mailbox of 'a Queue.T Synchronized.var;
    21 
    22 fun create () = Mailbox (Synchronized.var "mailbox" Queue.empty);
    23 
    24 fun send (Mailbox mailbox) msg =
    25   Synchronized.change mailbox (Queue.enqueue msg);
    26 
    27 fun receive (Mailbox mailbox) =
    28   Synchronized.guarded_access mailbox (try Queue.dequeue);
    29 
    30 fun receive_timeout timeout (Mailbox mailbox) =
    31   Synchronized.timed_access mailbox
    32     (fn _ => SOME (Time.+ (Time.now (), timeout))) (try Queue.dequeue);
    33 
    34 end;