# 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)
+}