--- 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