src/Pure/Concurrent/delay.scala
changeset 73367 77ef8bef0593
parent 71704 b9a5eb0f3b43
child 75380 2cb2606ce075
equal deleted inserted replaced
73366:5f388e514ab8 73367:77ef8bef0593
    35 
    35 
    36   def invoke(): Unit = synchronized
    36   def invoke(): Unit = synchronized
    37   {
    37   {
    38     val new_run =
    38     val new_run =
    39       running match {
    39       running match {
    40         case Some(request) => if (first) false else { request.cancel; true }
    40         case Some(request) => if (first) false else { request.cancel(); true }
    41         case None => true
    41         case None => true
    42       }
    42       }
    43     if (new_run)
    43     if (new_run)
    44       running = Some(Event_Timer.request(Time.now() + delay)(run))
    44       running = Some(Event_Timer.request(Time.now() + delay)(run))
    45   }
    45   }
    46 
    46 
    47   def revoke(): Unit = synchronized
    47   def revoke(): Unit = synchronized
    48   {
    48   {
    49     running match {
    49     running match {
    50       case Some(request) => request.cancel; running = None
    50       case Some(request) => request.cancel(); running = None
    51       case None =>
    51       case None =>
    52     }
    52     }
    53   }
    53   }
    54 
    54 
    55   def postpone(alt_delay: Time): Unit = synchronized
    55   def postpone(alt_delay: Time): Unit = synchronized
    56   {
    56   {
    57     running match {
    57     running match {
    58       case Some(request) =>
    58       case Some(request) =>
    59         val alt_time = Time.now() + alt_delay
    59         val alt_time = Time.now() + alt_delay
    60         if (request.time < alt_time && request.cancel) {
    60         if (request.time < alt_time && request.cancel()) {
    61           running = Some(Event_Timer.request(alt_time)(run))
    61           running = Some(Event_Timer.request(alt_time)(run))
    62         }
    62         }
    63       case None =>
    63       case None =>
    64     }
    64     }
    65   }
    65   }