author | wenzelm |
Tue, 05 Mar 2024 17:27:16 +0100 | |
changeset 79780 | 8e17f585177f |
parent 79779 | f1c9e9e4616d |
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 { |
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
11 |
def make_file(log_file: Option[Path], guard_time: Time = Time.min): Logger = |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
12 |
log_file match { |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
13 |
case Some(file) => new File_Logger(file, guard_time) |
79777 | 14 |
case None => new Logger |
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
15 |
} |
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
|
16 |
|
79780 | 17 |
def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger = { |
18 |
val t = guard_time |
|
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
19 |
new Logger { |
79780 | 20 |
override val guard_time: Time = t |
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
21 |
override def output(msg: => String): Unit = |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
22 |
if (progress != null) progress.echo(msg) |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
23 |
} |
79780 | 24 |
} |
77511 | 25 |
|
79779 | 26 |
def make_system_log(progress: => Progress, options: Options, guard_time: Time = Time.min): Logger = |
77511 | 27 |
options.string("system_log") match { |
79777 | 28 |
case "" => new Logger |
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
29 |
case "-" => make_progress(progress, guard_time = guard_time) |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
30 |
case log_file => make_file(Some(Path.explode(log_file)), guard_time = guard_time) |
77511 | 31 |
} |
64605 | 32 |
} |
33 |
||
79777 | 34 |
class Logger { |
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
35 |
val guard_time: Time = Time.min |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
36 |
def guard(t: Time): Boolean = t >= guard_time |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
37 |
def output(msg: => String): Unit = {} |
65921 | 38 |
|
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
39 |
final def apply(msg: => String, time: Option[Time] = None): Unit = |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
40 |
if (time.isEmpty || guard(time.get)) output(msg) |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
41 |
|
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
42 |
final def timeit[A](body: => A, |
76592 | 43 |
message: Exn.Result[A] => String = null, |
44 |
enabled: Boolean = true |
|
76593
badb5264f7b9
clarified signature: just one level of arguments to avoid type-inference problems;
wenzelm
parents:
76592
diff
changeset
|
45 |
): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_)) |
64605 | 46 |
} |
47 |
||
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
48 |
class File_Logger(path: Path, override val guard_time: Time = Time.min) |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
49 |
extends Logger { |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
50 |
override def output(msg: => String): Unit = synchronized { File.append(path, msg + "\n") } |
64605 | 51 |
override def toString: String = path.toString |
52 |
} |
|
77182 | 53 |
|
79775
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
54 |
class System_Logger(override val guard_time: Time = Time.min) |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
55 |
extends Logger { |
752806151432
clarified signature: incorporate guard into Logger;
wenzelm
parents:
79767
diff
changeset
|
56 |
override def output(msg: => String): Unit = synchronized { |
79778
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
57 |
if (System.console != null && System.console.writer != null) { |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
58 |
System.console.writer.println(msg) |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
59 |
System.console.writer.flush() |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
60 |
} |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
61 |
else if (System.out != null) { |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
62 |
System.out.println(msg) |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
63 |
System.out.flush() |
42c3e6dc57d9
more robust, notably for remote process (via SSH);
wenzelm
parents:
79777
diff
changeset
|
64 |
} |
77286 | 65 |
} |
77182 | 66 |
} |