src/Pure/General/logger.scala

--- a/src/Pure/General/logger.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/General/logger.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -11,7 +11,7 @@
   def make_file(log_file: Option[Path], guard_time: Time = Time.min): Logger =
     log_file match {
       case Some(file) => new File_Logger(file, guard_time)
-      case None => No_Logger
+      case None => new Logger
     }
 
   def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger =
@@ -22,13 +22,13 @@
 
   def make_system_log(progress: Progress, options: Options, guard_time: Time = Time.min): Logger =
     options.string("system_log") match {
-      case "" => No_Logger
+      case "" => new Logger
       case "-" => make_progress(progress, guard_time = guard_time)
       case log_file => make_file(Some(Path.explode(log_file)), guard_time = guard_time)
     }
 }
 
-trait Logger {
+class Logger {
   val guard_time: Time = Time.min
   def guard(t: Time): Boolean = t >= guard_time
   def output(msg: => String): Unit = {}
@@ -42,8 +42,6 @@
   ): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_))
 }
 
-object No_Logger extends Logger
-
 class File_Logger(path: Path, override val guard_time: Time = Time.min)
 extends Logger {
   override def output(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }