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 |
}
|