equal
deleted
inserted
replaced
9 |
9 |
10 object Logger |
10 object Logger |
11 { |
11 { |
12 def make(log_file: Option[Path]): Logger = |
12 def make(log_file: Option[Path]): Logger = |
13 log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } |
13 log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } |
|
14 |
|
15 def make(progress: Progress): Logger = |
|
16 new Logger { def apply(msg: => String): Unit = progress.echo(msg) } |
14 } |
17 } |
15 |
18 |
16 trait Logger |
19 trait Logger |
17 { |
20 { |
18 def apply(msg: => String): Unit |
21 def apply(msg: => String): Unit |