src/Pure/Concurrent/consumer_thread.scala
Thu, 17 Aug 2023 16:15:25 +0200 wenzelm clarified main_loop: support timeout, which results in consume(Nil);
Thu, 17 Aug 2023 15:12:18 +0200 wenzelm tuned;
less more (0) -10 -2 tip