src/Pure/General/logger.scala
author wenzelm
Sat, 05 Jun 2021 20:20:25 +0200
changeset 73814 c8b4a4f69068
parent 73777 52e43a93d51f
child 75393 87ebf5a50283
permissions -rw-r--r--
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);

/*  Title:      Pure/General/logger.scala
    Author:     Makarius

Minimal logging support.
*/

package isabelle


object Logger
{
  def make(log_file: Option[Path]): Logger =
    log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }

  def make(progress: Progress): Logger =
    new Logger { def apply(msg: => String): Unit = progress.echo(msg) }
}

trait Logger
{
  def apply(msg: => String): Unit

  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
    Timing.timeit(message, enabled, apply(_))(e)
}

object No_Logger extends Logger
{
  def apply(msg: => String): Unit = {}
}

class File_Logger(path: Path) extends Logger
{
  def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }

  override def toString: String = path.toString
}