src/Pure/Concurrent/mailbox.ML
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Fri, 27 Jun 2014 22:08:55 +0200 wenzelm more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
Wed, 10 Jul 2013 22:56:48 +0200 wenzelm explicit shutdown of message output thread;
Mon, 19 Jan 2009 19:38:03 +0100 wenzelm removed Ids;
Tue, 14 Oct 2008 13:01:52 +0200 wenzelm simplified synchronized variable access;
Mon, 13 Oct 2008 15:48:38 +0200 wenzelm simplified implementation using Synchronized.var;
Wed, 01 Oct 2008 12:00:02 +0200 wenzelm more robust treatment of Interrupt (cf. exn.ML);
Mon, 08 Sep 2008 22:14:39 +0200 wenzelm send: broadcast condition while locked!
Mon, 08 Sep 2008 20:35:38 +0200 wenzelm tuned Mailbox.send;
Sun, 07 Sep 2008 22:19:58 +0200 wenzelm tuned;
Sun, 07 Sep 2008 17:46:38 +0200 wenzelm send: broadcast to all waiting threads;
Thu, 04 Sep 2008 21:12:06 +0200 wenzelm proper header;
Thu, 04 Sep 2008 21:02:42 +0200 wenzelm added receive_timeout;
Thu, 04 Sep 2008 19:45:13 +0200 wenzelm Concurrent message exchange via mailbox -- with unbounded queueing.
less more (0) tip