src/Pure/Concurrent/simple_thread.scala
author wenzelm
Thu Apr 24 22:20:36 2014 +0200 (2014-04-24)
changeset 56707 aa4631879df8
parent 56704 c2f0ddd14747
child 56730 e723f041b6d0
permissions -rw-r--r--
obsolete;
wenzelm@38636
     1
/*  Title:      Pure/Concurrent/simple_thread.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@38636
     3
    Author:     Makarius
wenzelm@38636
     4
wenzelm@38636
     5
Simplified thread operations.
wenzelm@38636
     6
*/
wenzelm@38636
     7
wenzelm@38636
     8
package isabelle
wenzelm@38636
     9
wenzelm@38636
    10
wenzelm@38636
    11
import java.lang.Thread
wenzelm@38636
    12
wenzelm@38636
    13
wenzelm@38636
    14
object Simple_Thread
wenzelm@38636
    15
{
wenzelm@56667
    16
  /* pending interrupts */
wenzelm@49471
    17
wenzelm@49471
    18
  def interrupted_exception(): Unit =
wenzelm@56667
    19
    if (Thread.interrupted()) throw Exn.Interrupt()
wenzelm@49471
    20
wenzelm@49471
    21
wenzelm@38636
    22
  /* plain thread */
wenzelm@38636
    23
wenzelm@39577
    24
  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
wenzelm@38636
    25
  {
wenzelm@39577
    26
    val thread =
wenzelm@39577
    27
      if (name == null || name == "") new Thread() { override def run = body }
wenzelm@39577
    28
      else new Thread(name) { override def run = body }
wenzelm@38638
    29
    thread.setDaemon(daemon)
wenzelm@38636
    30
    thread.start
wenzelm@38636
    31
    thread
wenzelm@38636
    32
  }
wenzelm@38636
    33
wenzelm@39579
    34
wenzelm@39579
    35
  /* future result via thread */
wenzelm@39577
    36
wenzelm@48355
    37
  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
wenzelm@39577
    38
  {
wenzelm@39577
    39
    val result = Future.promise[A]
wenzelm@48355
    40
    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
wenzelm@48355
    41
    (thread, result)
wenzelm@39577
    42
  }
wenzelm@38636
    43
}
wenzelm@38636
    44