equal
deleted
inserted
replaced
11 def make(log_file: Option[Path]): Logger = |
11 def make(log_file: Option[Path]): Logger = |
12 log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } |
12 log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } |
13 |
13 |
14 def make(progress: Progress): Logger = |
14 def make(progress: Progress): Logger = |
15 new Logger { def apply(msg: => String): Unit = progress.echo(msg) } |
15 new Logger { def apply(msg: => String): Unit = progress.echo(msg) } |
|
16 |
|
17 def make_system_log(progress: Progress, options: Options): Logger = |
|
18 options.string("system_log") match { |
|
19 case "" => No_Logger |
|
20 case "-" => make(progress) |
|
21 case log_file => make(Some(Path.explode(log_file))) |
|
22 } |
16 } |
23 } |
17 |
24 |
18 trait Logger { |
25 trait Logger { |
19 def apply(msg: => String): Unit |
26 def apply(msg: => String): Unit |
20 |
27 |