src/Pure/Concurrent/event_timer.ML
2016-04-02 ago prefer infix operations;
2016-01-24 ago tuned;
2015-11-03 ago clarified modules;
2015-07-21 ago more explicit thread identification;
2015-01-29 ago explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
2015-01-10 ago tuned;
2015-01-10 ago tuned;
2015-01-09 ago clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
2014-04-28 ago added Scala version of module Event_Timer;
2013-07-30 ago recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-11 ago tuned;
2013-07-05 ago more uniform Counter in ML and Scala;
2013-05-17 ago event timer as separate service thread;