author | wenzelm |
Sat, 04 Mar 2023 23:43:53 +0100 | |
changeset 77511 | 3d6db917bd1b |
parent 77286 | 6435b0fd48b5 |
child 79767 | 52b5c7c8e6d9 |
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 |
||
75393 | 10 |
object Logger { |
64605 | 11 |
def make(log_file: Option[Path]): Logger = |
12 |
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
|
13 |
|
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 |
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
|
15 |
new Logger { def apply(msg: => String): Unit = progress.echo(msg) } |
77511 | 16 |
|
17 |
def make_system_log(progress: Progress, options: Options): Logger = |
|
18 |
options.string("system_log") match { |
|
19 |
case "" => No_Logger |
|
20 |
case "-" => make(progress) |
|
21 |
case log_file => make(Some(Path.explode(log_file))) |
|
22 |
} |
|
64605 | 23 |
} |
24 |
||
75393 | 25 |
trait Logger { |
64605 | 26 |
def apply(msg: => String): Unit |
65921 | 27 |
|
76593
badb5264f7b9
clarified signature: just one level of arguments to avoid type-inference problems;
wenzelm
parents:
76592
diff
changeset
|
28 |
def timeit[A](body: => A, |
76592 | 29 |
message: Exn.Result[A] => String = null, |
30 |
enabled: Boolean = true |
|
76593
badb5264f7b9
clarified signature: just one level of arguments to avoid type-inference problems;
wenzelm
parents:
76592
diff
changeset
|
31 |
): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_)) |
64605 | 32 |
} |
33 |
||
75393 | 34 |
object No_Logger extends Logger { |
73340 | 35 |
def apply(msg: => String): Unit = {} |
64605 | 36 |
} |
37 |
||
75393 | 38 |
class File_Logger(path: Path) extends Logger { |
73340 | 39 |
def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") } |
64605 | 40 |
|
41 |
override def toString: String = path.toString |
|
42 |
} |
|
77182 | 43 |
|
44 |
class System_Logger extends Logger { |
|
77286 | 45 |
def apply(msg: => String): Unit = synchronized { |
77182 | 46 |
if (Platform.is_windows) System.out.println(msg) |
47 |
else System.console.writer.println(msg) |
|
77286 | 48 |
} |
77182 | 49 |
} |