src/Pure/Concurrent/synchronized.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-16 wenzelm 2009-09-16 Synchronized.value does not require locking, since assigments are atomic; removed obsolete Synchronized.peek;
2009-08-01 wenzelm 2009-08-01 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts; renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts; added Multithreading.sync_interrupts; Multithreading.sync_wait: more careful treatment of attributes; Multithreading.tracing: uninterruptible; Multithreading.system_out: signal within critical region, more careful sync_wait; eliminated redundant Thread.testInterrupt; Future.wait_timeout: uniform Multithreading.sync_wait; future scheduler: interruptible body (sync!), to improve reactivity; future_job: reject duplicate assignments -- system error; misc tuning;
2009-07-30 wenzelm 2009-07-30 added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
2009-07-28 wenzelm 2009-07-28 added unsynchronized Synchronized.peek;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-10-14 wenzelm 2008-10-14 added value; simplified synchronized variable access;
2008-10-13 wenzelm 2008-10-13 State variables with synchronized access.