src/Pure/Concurrent/simple_thread.scala
changeset 56860 dc71c3d0e909
parent 56770 e160ae47db94
child 59136 c2b23cb8a677
equal deleted inserted replaced
56856:d940ad3959c5 56860:dc71c3d0e909
    14 import scala.collection.parallel.ForkJoinTasks
    14 import scala.collection.parallel.ForkJoinTasks
    15 
    15 
    16 
    16 
    17 object Simple_Thread
    17 object Simple_Thread
    18 {
    18 {
    19   /* pending interrupts */
       
    20 
       
    21   def interrupted_exception(): Unit =
       
    22     if (Thread.interrupted()) throw Exn.Interrupt()
       
    23 
       
    24 
       
    25   /* plain thread */
    19   /* plain thread */
    26 
    20 
    27   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
    21   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
    28   {
    22   {
    29     val thread =
    23     val thread =