src/Pure/Concurrent/simple_thread.scala
changeset 61555 e27cfd2bf094
parent 61194 e4699ef5cf90
equal deleted inserted replaced
61552:078c9fd2e052 61555:e27cfd2bf094
    69     def invoke(): Unit = synchronized
    69     def invoke(): Unit = synchronized
    70     {
    70     {
    71       val new_run =
    71       val new_run =
    72         running match {
    72         running match {
    73           case Some(request) => if (first) false else { request.cancel; cancel(); true }
    73           case Some(request) => if (first) false else { request.cancel; cancel(); true }
    74           case None => true
    74           case None => cancel(); true
    75         }
    75         }
    76       if (new_run)
    76       if (new_run)
    77         running = Some(Event_Timer.request(Time.now() + delay)(run))
    77         running = Some(Event_Timer.request(Time.now() + delay)(run))
    78     }
    78     }
    79 
    79