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 => new Logger |
14 case None => new 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 val t = guard_time |
18 new Logger { |
19 new Logger { |
|
20 override val guard_time: Time = t |
19 override def output(msg: => String): Unit = |
21 override def output(msg: => String): Unit = |
20 if (progress != null) progress.echo(msg) |
22 if (progress != null) progress.echo(msg) |
21 } |
23 } |
|
24 } |
22 |
25 |
23 def make_system_log(progress: => Progress, options: Options, guard_time: Time = Time.min): Logger = |
26 def make_system_log(progress: => Progress, options: Options, guard_time: Time = Time.min): Logger = |
24 options.string("system_log") match { |
27 options.string("system_log") match { |
25 case "" => new Logger |
28 case "" => new Logger |
26 case "-" => make_progress(progress, guard_time = guard_time) |
29 case "-" => make_progress(progress, guard_time = guard_time) |