consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
authorwenzelm
Thu Apr 24 13:13:48 2014 +0200 (2014-04-24)
changeset 56695963732291084
parent 56694 c4e77643aad6
child 56696 ff782c5450bf
consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
src/Pure/Concurrent/consumer_thread.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Thu Apr 24 13:13:48 2014 +0200
     1.3 @@ -0,0 +1,29 @@
     1.4 +/*  Title:      Pure/Concurrent/consumer_thread.scala
     1.5 +    Module:     PIDE
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Consumer thread with unbounded queueing of requests.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +import scala.annotation.tailrec
    1.15 +
    1.16 +
    1.17 +class Consumer_Thread[A](name: String = "", daemon: Boolean = false)
    1.18 +{
    1.19 +  def consume(x: A) { }
    1.20 +  def finish() { }
    1.21 +
    1.22 +  private val mbox = Mailbox[Option[A]]
    1.23 +  @tailrec private def loop(): Unit =
    1.24 +    mbox.receive match {
    1.25 +      case Some(x) => consume(x); loop()
    1.26 +      case None => finish()
    1.27 +    }
    1.28 +  private val thread = Simple_Thread.fork(name, daemon) { loop() }
    1.29 +
    1.30 +  final def send(x: A) { mbox.send(Some(x)) }
    1.31 +  final def shutdown() { mbox.send(None); mbox.await_empty; thread.join }
    1.32 +}
     2.1 --- a/src/Pure/build-jars	Thu Apr 24 13:10:42 2014 +0200
     2.2 +++ b/src/Pure/build-jars	Thu Apr 24 13:13:48 2014 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  ## sources
     2.5  
     2.6  declare -a SOURCES=(
     2.7 +  Concurrent/consumer_thread.scala
     2.8    Concurrent/counter.scala
     2.9    Concurrent/future.scala
    2.10    Concurrent/mailbox.scala