diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/Concurrent/delay.scala --- a/src/Pure/Concurrent/delay.scala Thu Mar 31 21:48:08 2022 +0200 +++ b/src/Pure/Concurrent/delay.scala Thu Mar 31 21:51:19 2022 +0200 @@ -33,8 +33,7 @@ } } - def invoke(): Unit = synchronized - { + def invoke(): Unit = synchronized { val new_run = running match { case Some(request) => if (first) false else { request.cancel(); true } @@ -44,16 +43,14 @@ running = Some(Event_Timer.request(Time.now() + delay)(run)) } - def revoke(): Unit = synchronized - { + def revoke(): Unit = synchronized { running match { case Some(request) => request.cancel(); running = None case None => } } - def postpone(alt_delay: Time): Unit = synchronized - { + def postpone(alt_delay: Time): Unit = synchronized { running match { case Some(request) => val alt_time = Time.now() + alt_delay