src/Pure/General/logger.scala
changeset 79776 c3f07c950116
parent 79775 752806151432
child 79777 db9c6be8e236
equal deleted inserted replaced
79775:752806151432 79776:c3f07c950116
    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