equal
deleted
inserted
replaced
12 log_file match { |
12 log_file match { |
13 case Some(file) => new File_Logger(file, guard_time) |
13 case Some(file) => new File_Logger(file, guard_time) |
14 case None => No_Logger |
14 case None => No_Logger |
15 } |
15 } |
16 |
16 |
17 def make_progress(progress: Progress, guard_time: Time = Time.min): Logger = |
17 def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger = |
18 new Logger { |
18 new Logger { |
19 override def output(msg: => String): Unit = |
19 override def output(msg: => String): Unit = |
20 if (progress != null) progress.echo(msg) |
20 if (progress != null) progress.echo(msg) |
21 } |
21 } |
22 |
22 |