# HG changeset patch
# User wenzelm
# Date 1398338028 -7200
# Node ID 96373229108449d1998b6db551662208d97e7776
# Parent  c4e77643aad6bd127abb5af8b5b8911942e850da
consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);

diff -r c4e77643aad6 -r 963732291084 src/Pure/Concurrent/consumer_thread.scala
--- /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 }
+}
diff -r c4e77643aad6 -r 963732291084 src/Pure/build-jars
--- 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