# HG changeset patch
# User wenzelm
# Date 1677969833 -3600
# Node ID 3d6db917bd1b7d5806aca9bb79d633eba6e5aeae
# Parent  f5d6cd98b16aaabb24ba0c60d01b79f14d440d1e
clarified modules;

diff -r f5d6cd98b16a -r 3d6db917bd1b src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Sat Mar 04 23:25:30 2023 +0100
+++ b/src/Pure/General/logger.scala	Sat Mar 04 23:43:53 2023 +0100
@@ -13,6 +13,13 @@
 
   def make(progress: Progress): Logger =
     new Logger { def apply(msg: => String): Unit = progress.echo(msg) }
+
+  def make_system_log(progress: Progress, options: Options): Logger =
+    options.string("system_log") match {
+      case "" => No_Logger
+      case "-" => make(progress)
+      case log_file => make(Some(Path.explode(log_file)))
+    }
 }
 
 trait Logger {
diff -r f5d6cd98b16a -r 3d6db917bd1b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Mar 04 23:25:30 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Mar 04 23:43:53 2023 +0100
@@ -652,12 +652,7 @@
     override def stopped: Boolean = build_progress.stopped
   }
 
-  val log: Logger =
-    build_options.string("system_log") match {
-      case "" => No_Logger
-      case "-" => Logger.make(progress)
-      case log_file => Logger.make(Some(Path.explode(log_file)))
-    }
+  val log: Logger = Logger.make_system_log(progress, build_options)
 
 
   /* policy operations */