# HG changeset patch # User wenzelm # Date 1675437886 -3600 # Node ID 25dbf5bec91e22264c3dd80d9512f26ec37e1970 # Parent 3eb3de8677862aab91e2a0866cda80f91fb3a318 more logging; diff -r 3eb3de867786 -r 25dbf5bec91e src/Pure/Concurrent/delay.scala --- a/src/Pure/Concurrent/delay.scala Fri Feb 03 14:29:07 2023 +0100 +++ b/src/Pure/Concurrent/delay.scala Fri Feb 03 16:24:46 2023 +0100 @@ -30,7 +30,8 @@ } } - def invoke(): Unit = synchronized { + def invoke(msg: String = ""): Unit = synchronized { + if (msg.nonEmpty) log("Delay.invoke " + msg) val new_run = running match { case Some(request) => if (first) false else { request.cancel(); true } @@ -40,14 +41,16 @@ running = Some(Event_Timer.request(Time.now() + delay)(run)) } - def revoke(): Unit = synchronized { + def revoke(msg: String = ""): Unit = synchronized { + if (msg.nonEmpty) log("Delay.revoke " + msg) running match { case Some(request) => request.cancel(); running = None case None => } } - def postpone(alt_delay: Time): Unit = synchronized { + def postpone(alt_delay: Time, msg: String = ""): Unit = synchronized { + if (msg.nonEmpty) log("Delay.postpone " + msg) running match { case Some(request) => val alt_time = Time.now() + alt_delay diff -r 3eb3de867786 -r 25dbf5bec91e src/Pure/General/logger.scala --- a/src/Pure/General/logger.scala Fri Feb 03 14:29:07 2023 +0100 +++ b/src/Pure/General/logger.scala Fri Feb 03 16:24:46 2023 +0100 @@ -33,3 +33,9 @@ override def toString: String = path.toString } + +class System_Logger extends Logger { + def apply(msg: => String): Unit = + if (Platform.is_windows) System.out.println(msg) + else System.console.writer.println(msg) +}