--- 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 {
--- 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 */