src/Pure/Concurrent/standard_thread.scala
changeset 71682 c467a682f700
parent 71681 3622eea18e39
child 71683 fd487d261169
equal deleted inserted replaced
71681:3622eea18e39 71682:c467a682f700
    10 import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
    10 import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
    11 
    11 
    12 
    12 
    13 object Standard_Thread
    13 object Standard_Thread
    14 {
    14 {
       
    15   /* fork */
       
    16 
       
    17   private val counter = Counter.make()
       
    18 
       
    19   def make_name(name: String, base: String = "thread"): String =
       
    20     proper_string(name).getOrElse(base + counter())
       
    21 
    15   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Standard_Thread =
    22   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Standard_Thread =
    16   {
    23   {
    17     val thread = new Standard_Thread(name, daemon, body)
    24     val group = Thread.currentThread.getThreadGroup
       
    25     val main = new Runnable { override def run { body } }
       
    26     val thread = new Standard_Thread(group, main, make_name(name), daemon)
    18     thread.start
    27     thread.start
    19     thread
    28     thread
    20   }
    29   }
    21 
    30 
       
    31 
       
    32   /* self */
       
    33 
       
    34   def self: Option[Standard_Thread] =
       
    35     Thread.currentThread match {
       
    36       case thread: Standard_Thread => Some(thread)
       
    37       case _ => None
       
    38     }
       
    39 
    22   def uninterruptible[A](body: => A): A =
    40   def uninterruptible[A](body: => A): A =
    23   {
    41   {
    24     Thread.currentThread match {
    42     self match {
    25       case thread: Standard_Thread => thread.uninterruptible(body)
    43       case Some(thread) => thread.uninterruptible(body)
    26       case thread => error("uninterruptible: not a standard managed thread: " + thread)
    44       case None => error("Cannot change interrupts --- running on non-standard thread")
    27     }
    45     }
    28   }
    46   }
    29 
    47 
    30 
    48 
    31   /* pool */
    49   /* pool */
   107   // delayed event after last invocation
   125   // delayed event after last invocation
   108   def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
   126   def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
   109     new Delay(false, delay, log, event)
   127     new Delay(false, delay, log, event)
   110 }
   128 }
   111 
   129 
   112 class Standard_Thread private(name: String, daemon: Boolean, main: => Unit)
   130 class Standard_Thread private(group: ThreadGroup, main: Runnable, name: String, daemon: Boolean)
   113   extends Thread()
   131   extends Thread(group, null, name)
   114 {
   132 {
   115   thread =>
   133   thread =>
   116 
   134 
   117   proper_string(name).foreach(thread.setName)
       
   118   thread.setDaemon(daemon)
   135   thread.setDaemon(daemon)
   119 
   136 
   120   override def run { main }
   137   override def run { main.run() }
   121 
   138 
   122   private var interruptible: Boolean = true
   139   private var interruptible: Boolean = true
   123   private var interrupt_pending: Boolean = false
   140   private var interrupt_pending: Boolean = false
   124 
   141 
   125   override def interrupt: Unit = synchronized
   142   override def interrupt: Unit = synchronized
   126   {
   143   {
   127     if (interruptible) super.interrupt()
   144     if (interruptible) super.interrupt()
   128     else { interrupt_pending = true }
   145     else { interrupt_pending = true }
   129   }
   146   }
   130 
   147 
   131   private def uninterruptible[A](body: => A): A =
   148   def uninterruptible[A](body: => A): A =
   132   {
   149   {
       
   150     require(Thread.currentThread == thread)
       
   151 
   133     val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
   152     val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
   134     try { body }
   153     try { body }
   135     finally {
   154     finally {
   136       synchronized {
   155       synchronized {
   137         interruptible = interruptible0
   156         interruptible = interruptible0