| 64606 |      1 | /*  Title:      Pure/General/logger.scala
 | 
| 64605 |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Minimal logging support.
 | 
|  |      5 | */
 | 
|  |      6 | 
 | 
| 64606 |      7 | package isabelle
 | 
| 64605 |      8 | 
 | 
|  |      9 | 
 | 
|  |     10 | object Logger
 | 
|  |     11 | {
 | 
|  |     12 |   def make(log_file: Option[Path]): Logger =
 | 
|  |     13 |     log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
 | 
|  |     14 | }
 | 
|  |     15 | 
 | 
|  |     16 | trait Logger
 | 
|  |     17 | {
 | 
|  |     18 |   def apply(msg: => String): Unit
 | 
| 65921 |     19 | 
 | 
|  |     20 |   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
 | 
|  |     21 |     Timing.timeit(message, enabled, apply(_))(e)
 | 
| 64605 |     22 | }
 | 
|  |     23 | 
 | 
|  |     24 | object No_Logger extends Logger
 | 
|  |     25 | {
 | 
|  |     26 |   def apply(msg: => String) { }
 | 
|  |     27 | }
 | 
|  |     28 | 
 | 
|  |     29 | class File_Logger(path: Path) extends Logger
 | 
|  |     30 | {
 | 
|  |     31 |   def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
 | 
|  |     32 | 
 | 
|  |     33 |   override def toString: String = path.toString
 | 
|  |     34 | }
 |