author | wenzelm |
Sat, 04 Sep 2021 21:25:08 +0200 | |
changeset 74232 | 1091880266e5 |
parent 73777 | 52e43a93d51f |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
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 } |
|
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73340
diff
changeset
|
14 |
|
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73340
diff
changeset
|
15 |
def make(progress: Progress): Logger = |
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73340
diff
changeset
|
16 |
new Logger { def apply(msg: => String): Unit = progress.echo(msg) } |
64605 | 17 |
} |
18 |
||
19 |
trait Logger |
|
20 |
{ |
|
21 |
def apply(msg: => String): Unit |
|
65921 | 22 |
|
23 |
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
|
24 |
Timing.timeit(message, enabled, apply(_))(e) |
|
64605 | 25 |
} |
26 |
||
27 |
object No_Logger extends Logger |
|
28 |
{ |
|
73340 | 29 |
def apply(msg: => String): Unit = {} |
64605 | 30 |
} |
31 |
||
32 |
class File_Logger(path: Path) extends Logger |
|
33 |
{ |
|
73340 | 34 |
def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") } |
64605 | 35 |
|
36 |
override def toString: String = path.toString |
|
37 |
} |