# HG changeset patch
# User wenzelm
# Date 1698763246 -3600
# Node ID 2024a2298d7a750ee6282ccda9454b033a619d7b
# Parent  f627ab8c276ca83297cfe8c60353a2201293fd0a
tuned signature;

diff -r f627ab8c276c -r 2024a2298d7a src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Oct 31 14:35:51 2023 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Oct 31 15:40:46 2023 +0100
@@ -45,7 +45,7 @@
   /* thread */
 
   private var active = true
-  private val mailbox = Mailbox[Option[Request]]
+  private val mailbox = Mailbox[Option[Request]]()
 
   private val thread = Isabelle_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
   def is_active(): Boolean = active && thread.isAlive
diff -r f627ab8c276c -r 2024a2298d7a src/Pure/Concurrent/mailbox.scala
--- a/src/Pure/Concurrent/mailbox.scala	Tue Oct 31 14:35:51 2023 +0100
+++ b/src/Pure/Concurrent/mailbox.scala	Tue Oct 31 15:40:46 2023 +0100
@@ -9,7 +9,7 @@
 
 
 object Mailbox {
-  def apply[A]: Mailbox[A] = new Mailbox[A]()
+  def apply[A](): Mailbox[A] = new Mailbox[A]()
 }
 
 
@@ -23,6 +23,6 @@
     (mailbox.timed_access(_ => timeout.map(t => Time.now() + t),
       { case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse
 
-  def await_empty: Unit =
+  def await_empty(): Unit =
     mailbox.guarded_access({ case Nil => Some(((), Nil)) case _ => None })
 }