# HG changeset patch
# User wenzelm
# Date 1574265363 -3600
# Node ID d6b9dead8c8d507141ab0368bff6ea8805b13b56
# Parent  5ea3ed3c52b35a44506d8142c113ddda7d230749
tuned signature;

diff -r 5ea3ed3c52b3 -r d6b9dead8c8d src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Wed Nov 20 16:28:13 2019 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala	Wed Nov 20 16:56:03 2019 +0100
@@ -85,7 +85,7 @@
 
   @tailrec private def main_loop(msgs: List[Option[Request]]): Unit =
     msgs match {
-      case Nil => main_loop(mailbox.receive(None))
+      case Nil => main_loop(mailbox.receive())
       case None :: _ => robust_finish()
       case _ =>
         val reqs =
@@ -106,7 +106,7 @@
 
         if (continue) {
           val msgs1 = msgs.drop(reqs.length)
-          val msgs2 = mailbox.receive(Some(Time.zero))
+          val msgs2 = mailbox.receive(timeout = Some(Time.zero))
           main_loop(msgs1 ::: msgs2)
         }
         else robust_finish()
diff -r 5ea3ed3c52b3 -r d6b9dead8c8d src/Pure/Concurrent/mailbox.scala
--- a/src/Pure/Concurrent/mailbox.scala	Wed Nov 20 16:28:13 2019 +0100
+++ b/src/Pure/Concurrent/mailbox.scala	Wed Nov 20 16:56:03 2019 +0100
@@ -21,7 +21,7 @@
 
   def send(msg: A): Unit = mailbox.change(msg :: _)
 
-  def receive(timeout: Option[Time]): List[A] =
+  def receive(timeout: Option[Time] = None): List[A] =
     (mailbox.timed_access(_ => timeout.map(t => Time.now() + t),
       { case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse