src/Pure/General/logger.scala
changeset 79780 8e17f585177f
parent 79779 f1c9e9e4616d
equal deleted inserted replaced
79779:f1c9e9e4616d 79780:8e17f585177f
    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)