src/Pure/Concurrent/event_timer.ML
Tue, 30 Jul 2013 18:19:16 +0200 wenzelm recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
Thu, 11 Jul 2013 11:40:21 +0200 wenzelm tuned;
Fri, 05 Jul 2013 23:10:18 +0200 wenzelm more uniform Counter in ML and Scala;
Fri, 17 May 2013 17:11:06 +0200 wenzelm event timer as separate service thread;
less more (0) tip