# HG changeset patch
# User wenzelm
# Date 1709651166 -3600
# Node ID db9c6be8e236dad55e14586cabb5079762fccc27
# Parent  c3f07c950116e8b1000a7c5d66c22cabaf9bc38a
prefer dynamic objects, following a5fda30edae2;

diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -83,7 +83,7 @@
         val local_build_context = build_context.copy(store = Store(local_options))
 
         val build =
-          Build_Job.start_session(local_build_context, session, progress, No_Logger, server,
+          Build_Job.start_session(local_build_context, session, progress, new Logger, server,
             background, session.sources_shasum, input_shasum, node_info, false)
 
         val timing =
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Build/resources.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -24,7 +24,7 @@
 
 class Resources(
   val session_background: Sessions.Background,
-  val log: Logger = No_Logger,
+  val log: Logger = new Logger,
   command_timings: List[Properties.T] = Nil
 ) {
   resources =>
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Concurrent/delay.scala
--- a/src/Pure/Concurrent/delay.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Concurrent/delay.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -9,11 +9,11 @@
 
 object Delay {
   // delayed event after first invocation
-  def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+  def first(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
     new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
 
   // delayed event after last invocation
-  def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+  def last(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
     new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
 }
 
diff -r c3f07c950116 -r db9c6be8e236 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") }
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -448,7 +448,7 @@
     def apply(
       options: Options,
       session_background: Sessions.Background,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): Resources = new Resources(options, session_background, log = log)
 
     def make(
@@ -457,7 +457,7 @@
       session_dirs: List[Path] = Nil,
       include_sessions: List[String] = Nil,
       progress: Progress = new Progress,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): Resources = {
       val session_background =
         Sessions.background(options, session_name, dirs = session_dirs,
@@ -605,7 +605,7 @@
   class Resources private[Headless](
     val options: Options,
     session_background: Sessions.Background,
-    log: Logger = No_Logger)
+    log: Logger = new Logger)
   extends isabelle.Resources(session_background.check_errors, log = log) {
     resources =>
 
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Tools/dump.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -142,7 +142,7 @@
 
     def sessions(
       logic: String = default_logic,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): List[Session] = {
       /* partitions */
 
@@ -359,7 +359,7 @@
     logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = new Progress,
-    log: Logger = No_Logger,
+    log: Logger = new Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Tools/server.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -397,7 +397,7 @@
     name: String = default_name,
     port: Int = 0,
     existing_server: Boolean = false,
-    log: Logger = No_Logger
+    log: Logger = new Logger
   ): (Info, Option[Server]) = {
     using(SQLite.open_database(private_data.database, restrict = true)) { db =>
       private_data.transaction_lock(db, create = true) {
diff -r c3f07c950116 -r db9c6be8e236 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Pure/Tools/server_commands.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -123,7 +123,7 @@
     def command(
       args: Args,
       progress: Progress = new Progress,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
       val (_, _, options, session_background) =
         try { Session_Build.command(args.build, progress = progress) }
diff -r c3f07c950116 -r db9c6be8e236 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -17,7 +17,7 @@
 class Channel(
   in: InputStream,
   out: OutputStream,
-  log: Logger = No_Logger,
+  log: Logger = new Logger,
   verbose: Boolean = false
 ) {
   /* read message */
diff -r c3f07c950116 -r db9c6be8e236 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -91,7 +91,7 @@
         }
         catch {
           case exn: Throwable =>
-            val channel = new Channel(System.in, System.out, No_Logger)
+            val channel = new Channel(System.in, System.out, new Logger)
             channel.error_message(Exn.message(exn))
             throw(exn)
         }
@@ -108,7 +108,7 @@
   session_requirements: Boolean = false,
   session_no_build: Boolean = false,
   modes: List[String] = Nil,
-  log: Logger = No_Logger
+  log: Logger = new Logger
 ) {
   server =>
 
diff -r c3f07c950116 -r db9c6be8e236 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 05 15:58:45 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 05 16:06:06 2024 +0100
@@ -70,7 +70,7 @@
 class VSCode_Resources(
   val options: Options,
   session_background: Sessions.Background,
-  log: Logger = No_Logger)
+  log: Logger = new Logger)
 extends Resources(session_background, log = log) {
   resources =>