src/Pure/Concurrent/synchronized.ML
Thu, 18 Dec 2014 16:13:54 +0100 wenzelm peek value without synchronization;
Fri, 12 Dec 2014 14:31:57 +0100 wenzelm Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
Wed, 26 Nov 2014 11:43:51 +0100 wenzelm load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
Thu, 24 Apr 2014 12:09:55 +0200 wenzelm synchronized access, similar to ML version;
Thu, 24 Apr 2014 00:27:06 +0200 wenzelm more uniform synchronized variables;
Fri, 05 Jul 2013 23:10:18 +0200 wenzelm more uniform Counter in ML and Scala;
Fri, 05 Jul 2013 15:38:03 +0200 wenzelm explicit module Document_ID as source of globally unique identifiers across ML/Scala;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Sun, 10 Jul 2011 16:13:37 +0200 wenzelm made SML/NJ happy;
Tue, 09 Nov 2010 21:44:19 +0100 wenzelm added general Synchronized.counter convenience;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 06 Feb 2010 22:05:02 +0100 wenzelm removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
Thu, 22 Oct 2009 15:19:44 +0200 wenzelm support single-assigment variables -- based on magic RTS operations by David Matthews;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 16 Sep 2009 22:46:10 +0200 wenzelm Synchronized.value does not require locking, since assigments are atomic;
Sat, 01 Aug 2009 00:09:45 +0200 wenzelm renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
Thu, 30 Jul 2009 23:06:06 +0200 wenzelm added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
Tue, 28 Jul 2009 15:05:18 +0200 wenzelm added unsynchronized Synchronized.peek;
Mon, 19 Jan 2009 19:38:03 +0100 wenzelm removed Ids;
Tue, 14 Oct 2008 13:01:56 +0200 wenzelm added value;
Mon, 13 Oct 2008 15:48:40 +0200 wenzelm State variables with synchronized access.
less more (0) tip