src/Pure/Concurrent/simple_thread.ML
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-25 wenzelm 2009-07-25 tuned tracing;
2009-07-25 wenzelm 2009-07-25 added Multithreading.real_time;
2009-07-25 wenzelm 2009-07-25 simplified/unified Multithreading.tracing_time; tuned;
2009-07-18 wenzelm 2009-07-18 synchronized: tuned tracing;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-10-13 wenzelm 2008-10-13 added generic combinator for synchronized evaluation (formerly in future.ML);
2008-10-09 wenzelm 2008-10-09 added fail-safe interrupt;
2008-09-16 wenzelm 2008-09-16 Simplified thread fork interface.