src/Pure/Concurrent/simple_thread.scala
author wenzelm
Thu, 24 Apr 2014 22:20:36 +0200
changeset 56707 aa4631879df8
parent 56704 c2f0ddd14747
child 56730 e723f041b6d0
permissions -rw-r--r--
obsolete;

/*  Title:      Pure/Concurrent/simple_thread.scala
    Module:     PIDE
    Author:     Makarius

Simplified thread operations.
*/

package isabelle


import java.lang.Thread


object Simple_Thread
{
  /* pending interrupts */

  def interrupted_exception(): Unit =
    if (Thread.interrupted()) throw Exn.Interrupt()


  /* plain thread */

  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
  {
    val thread =
      if (name == null || name == "") new Thread() { override def run = body }
      else new Thread(name) { override def run = body }
    thread.setDaemon(daemon)
    thread.start
    thread
  }


  /* future result via thread */

  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
  {
    val result = Future.promise[A]
    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    (thread, result)
  }
}