src/Pure/Concurrent/standard_thread.scala
author wenzelm
Tue Nov 03 16:35:38 2015 +0100 (2015-11-03)
changeset 61559 313eca3fa847
parent 61556 0d4ee4168e41
child 61563 91c3aedbfc5e
permissions -rw-r--r--
more direct task future implementation, with proper cancel operation;
more uniform Future.thread;
wenzelm@61556
     1
/*  Title:      Pure/Concurrent/standard_thread.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@38636
     3
    Author:     Makarius
wenzelm@38636
     4
wenzelm@61556
     5
Standard 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@59136
    12
import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
wenzelm@59136
    13
  TimeUnit, LinkedBlockingQueue}
wenzelm@38636
    14
wenzelm@38636
    15
wenzelm@61556
    16
object Standard_Thread
wenzelm@38636
    17
{
wenzelm@38636
    18
  /* plain thread */
wenzelm@38636
    19
wenzelm@39577
    20
  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
wenzelm@38636
    21
  {
wenzelm@39577
    22
    val thread =
wenzelm@39577
    23
      if (name == null || name == "") new Thread() { override def run = body }
wenzelm@39577
    24
      else new Thread(name) { override def run = body }
wenzelm@38638
    25
    thread.setDaemon(daemon)
wenzelm@38636
    26
    thread.start
wenzelm@38636
    27
    thread
wenzelm@38636
    28
  }
wenzelm@38636
    29
wenzelm@39579
    30
wenzelm@56730
    31
  /* thread pool */
wenzelm@56730
    32
wenzelm@61559
    33
  lazy val pool: ThreadPoolExecutor =
wenzelm@59136
    34
    {
wenzelm@59136
    35
      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
wenzelm@59136
    36
      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
wenzelm@59136
    37
      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
wenzelm@59136
    38
    }
wenzelm@56730
    39
wenzelm@56730
    40
  def submit_task[A](body: => A): JFuture[A] =
wenzelm@61559
    41
    pool.submit(new Callable[A] { def call = body })
wenzelm@56770
    42
wenzelm@56770
    43
wenzelm@56770
    44
  /* delayed events */
wenzelm@56770
    45
wenzelm@61556
    46
  final class Delay private [Standard_Thread](
wenzelm@61194
    47
    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
wenzelm@56770
    48
  {
wenzelm@56770
    49
    private var running: Option[Event_Timer.Request] = None
wenzelm@56770
    50
wenzelm@56770
    51
    private def run: Unit =
wenzelm@56770
    52
    {
wenzelm@56770
    53
      val do_run = synchronized {
wenzelm@56770
    54
        if (running.isDefined) { running = None; true } else false
wenzelm@56770
    55
      }
wenzelm@56770
    56
      if (do_run) event
wenzelm@56770
    57
    }
wenzelm@56770
    58
wenzelm@56770
    59
    def invoke(): Unit = synchronized
wenzelm@56770
    60
    {
wenzelm@56770
    61
      val new_run =
wenzelm@56770
    62
        running match {
wenzelm@61194
    63
          case Some(request) => if (first) false else { request.cancel; cancel(); true }
wenzelm@61555
    64
          case None => cancel(); true
wenzelm@56770
    65
        }
wenzelm@56770
    66
      if (new_run)
wenzelm@56770
    67
        running = Some(Event_Timer.request(Time.now() + delay)(run))
wenzelm@56770
    68
    }
wenzelm@56770
    69
wenzelm@56770
    70
    def revoke(): Unit = synchronized
wenzelm@56770
    71
    {
wenzelm@56770
    72
      running match {
wenzelm@61194
    73
        case Some(request) => request.cancel; cancel(); running = None
wenzelm@61194
    74
        case None => cancel()
wenzelm@56770
    75
      }
wenzelm@56770
    76
    }
wenzelm@56770
    77
wenzelm@61194
    78
    def postpone(alt_delay: Time): Unit = synchronized
wenzelm@56770
    79
    {
wenzelm@56770
    80
      running match {
wenzelm@56770
    81
        case Some(request) =>
wenzelm@56770
    82
          val alt_time = Time.now() + alt_delay
wenzelm@56770
    83
          if (request.time < alt_time && request.cancel) {
wenzelm@61194
    84
            cancel()
wenzelm@56770
    85
            running = Some(Event_Timer.request(alt_time)(run))
wenzelm@56770
    86
          }
wenzelm@61194
    87
          else cancel()
wenzelm@61194
    88
        case None => cancel()
wenzelm@56770
    89
      }
wenzelm@56770
    90
    }
wenzelm@56770
    91
  }
wenzelm@56770
    92
wenzelm@56770
    93
  // delayed event after first invocation
wenzelm@61194
    94
  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
wenzelm@61194
    95
    new Delay(true, delay, cancel, event)
wenzelm@56770
    96
wenzelm@56770
    97
  // delayed event after last invocation
wenzelm@61194
    98
  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
wenzelm@61194
    99
    new Delay(false, delay, cancel, event)
wenzelm@38636
   100
}