author | wenzelm |
Sat, 01 Jun 2024 21:49:50 +0200 | |
changeset 80235 | 06036a16779f |
parent 80230 | cb4b21b7b473 |
child 80236 | c6670f9575de |
permissions | -rw-r--r-- |
61276 | 1 |
/* Title: Pure/System/progress.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Progress context for system processes. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
73897 | 10 |
import java.util.{Map => JMap} |
64201 | 11 |
|
12 |
||
75393 | 13 |
object Progress { |
78503 | 14 |
/* output */ |
15 |
||
16 |
sealed abstract class Output { def message: Message } |
|
78155 | 17 |
|
78611 | 18 |
enum Kind { case writeln, warning, error_message } |
78503 | 19 |
sealed case class Message( |
78611 | 20 |
kind: Kind, |
78503 | 21 |
text: String, |
22 |
verbose: Boolean = false |
|
23 |
) extends Output { |
|
24 |
override def message: Message = this |
|
25 |
||
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
26 |
def output_text: String = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
27 |
kind match { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
28 |
case Kind.writeln => Output.writeln_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
29 |
case Kind.warning => Output.warning_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
30 |
case Kind.error_message => Output.error_message_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
31 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
32 |
|
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
33 |
override def toString: String = output_text |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
34 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
35 |
|
78503 | 36 |
sealed case class Theory( |
37 |
theory: String, |
|
38 |
session: String = "", |
|
39 |
percentage: Option[Int] = None |
|
40 |
) extends Output { |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
41 |
def message: Message = |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
42 |
Message(Kind.writeln, print_session + print_theory + print_percentage, verbose = true) |
68987 | 43 |
|
77504 | 44 |
def print_session: String = if_proper(session, session + ": ") |
68987 | 45 |
def print_theory: String = "theory " + theory |
46 |
def print_percentage: String = |
|
47 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 48 |
} |
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
49 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
50 |
|
75393 | 51 |
class Progress { |
78876 | 52 |
def now(): Date = Date.now() |
53 |
val start: Date = now() |
|
54 |
||
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
55 |
def verbose: Boolean = false |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
56 |
final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
57 |
|
78432 | 58 |
def output(message: Progress.Message): Unit = {} |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
59 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
60 |
final def echo(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
61 |
output(Progress.Message(Progress.Kind.writeln, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
62 |
final def echo_warning(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
63 |
output(Progress.Message(Progress.Kind.warning, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
64 |
final def echo_error_message(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
65 |
output(Progress.Message(Progress.Kind.error_message, msg, verbose = verbose)) |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
66 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
67 |
final def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg) |
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
68 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
69 |
def theory(theory: Progress.Theory): Unit = output(theory.message) |
73340 | 70 |
def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} |
64909 | 71 |
|
78432 | 72 |
final def capture[A](e: => A, msg: String, err: Throwable => String): Exn.Result[A] = { |
73 |
echo(msg) |
|
74 |
try { Exn.Res(e) } |
|
75 |
catch { case exn: Throwable => echo_error_message(err(exn)); Exn.Exn[A](exn) } |
|
76 |
} |
|
77 |
||
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
78 |
final def timeit[A]( |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
79 |
body: => A, |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
80 |
message: Exn.Result[A] => String = null, |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
81 |
enabled: Boolean = true |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
82 |
): A = Timing.timeit(body, message = message, enabled = enabled, output = echo(_)) |
65921 | 83 |
|
77524 | 84 |
@volatile private var is_stopped = false |
73367 | 85 |
def stop(): Unit = { is_stopped = true } |
75393 | 86 |
def stopped: Boolean = { |
73367 | 87 |
if (Thread.interrupted()) is_stopped = true |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
88 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
89 |
} |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
90 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
91 |
final def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
92 |
final def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() |
61276 | 93 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 94 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
95 |
final def bash(script: String, |
80230 | 96 |
ssh: SSH.System = SSH.Local, |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
79887
diff
changeset
|
97 |
cwd: Path = Path.current, |
80230 | 98 |
env: JMap[String, String] = Isabelle_System.settings(), // ignored for remote ssh |
64201 | 99 |
redirect: Boolean = false, |
65930 | 100 |
echo: Boolean = false, |
72599 | 101 |
watchdog: Time = Time.zero, |
75393 | 102 |
strict: Boolean = true |
103 |
): Process_Result = { |
|
72599 | 104 |
val result = |
80230 | 105 |
Isabelle_System.bash(script, ssh = ssh, cwd = cwd, env = env, redirect = redirect, |
72599 | 106 |
progress_stdout = echo_if(echo, _), |
107 |
progress_stderr = echo_if(echo, _), |
|
80235 | 108 |
watchdog = Bash.Watchdog(watchdog, _ => stopped), |
72599 | 109 |
strict = strict) |
110 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 111 |
} |
61276 | 112 |
} |
113 |
||
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
114 |
class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false) |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
115 |
extends Progress { |
78874 | 116 |
override def output(message: Progress.Message): Unit = synchronized { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
117 |
if (do_output(message)) { |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
118 |
Output.output(message.output_text, stdout = !stderr, include_empty = true) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
119 |
} |
78874 | 120 |
} |
77503 | 121 |
|
122 |
override def toString: String = super.toString + ": console" |
|
61276 | 123 |
} |
65888 | 124 |
|
77507 | 125 |
class File_Progress(path: Path, override val verbose: Boolean = false) |
126 |
extends Progress { |
|
78874 | 127 |
override def output(message: Progress.Message): Unit = synchronized { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
128 |
if (do_output(message)) File.append(path, message.output_text + "\n") |
78874 | 129 |
} |
65888 | 130 |
|
77503 | 131 |
override def toString: String = super.toString + ": " + path.toString |
65888 | 132 |
} |