consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/consumer_thread.scala	Thu Apr 24 13:13:48 2014 +0200
@@ -0,0 +1,29 @@
+/*  Title:      Pure/Concurrent/consumer_thread.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Consumer thread with unbounded queueing of requests.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+
+class Consumer_Thread[A](name: String = "", daemon: Boolean = false)
+{
+  def consume(x: A) { }
+  def finish() { }
+
+  private val mbox = Mailbox[Option[A]]
+  @tailrec private def loop(): Unit =
+    mbox.receive match {
+      case Some(x) => consume(x); loop()
+      case None => finish()
+    }
+  private val thread = Simple_Thread.fork(name, daemon) { loop() }
+
+  final def send(x: A) { mbox.send(Some(x)) }
+  final def shutdown() { mbox.send(None); mbox.await_empty; thread.join }
+}

--- a/src/Pure/build-jars	Thu Apr 24 13:10:42 2014 +0200
+++ b/src/Pure/build-jars	Thu Apr 24 13:13:48 2014 +0200
@@ -9,6 +9,7 @@
 ## sources
 
 declare -a SOURCES=(
+  Concurrent/consumer_thread.scala
   Concurrent/counter.scala
   Concurrent/future.scala
   Concurrent/mailbox.scala