author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73897 | 0ddb5de0506e |
child 76592 | ec8bf1268f45 |
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 |
import java.io.{File => JFile} |
12 |
||
13 |
||
75393 | 14 |
object Progress { |
15 |
sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) { |
|
68987 | 16 |
def message: String = print_session + print_theory + print_percentage |
17 |
||
18 |
def print_session: String = if (session == "") "" else session + ": " |
|
19 |
def print_theory: String = "theory " + theory |
|
20 |
def print_percentage: String = |
|
21 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 22 |
} |
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
23 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
24 |
|
75393 | 25 |
class Progress { |
73340 | 26 |
def echo(msg: String): Unit = {} |
27 |
def echo_if(cond: Boolean, msg: String): Unit = { if (cond) echo(msg) } |
|
28 |
def theory(theory: Progress.Theory): Unit = {} |
|
29 |
def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} |
|
64909 | 30 |
|
73340 | 31 |
def echo_warning(msg: String): Unit = echo(Output.warning_text(msg)) |
32 |
def echo_error_message(msg: String): Unit = echo(Output.error_message_text(msg)) |
|
65826 | 33 |
|
65921 | 34 |
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
71601 | 35 |
Timing.timeit(message, enabled, echo)(e) |
65921 | 36 |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
37 |
@volatile protected var is_stopped = false |
73367 | 38 |
def stop(): Unit = { is_stopped = true } |
75393 | 39 |
def stopped: Boolean = { |
73367 | 40 |
if (Thread.interrupted()) is_stopped = true |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
41 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
42 |
} |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
43 |
|
73367 | 44 |
def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } |
73340 | 45 |
def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() |
61276 | 46 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 47 |
|
48 |
def bash(script: String, |
|
49 |
cwd: JFile = null, |
|
73897 | 50 |
env: JMap[String, String] = Isabelle_System.settings(), |
64201 | 51 |
redirect: Boolean = false, |
65930 | 52 |
echo: Boolean = false, |
72599 | 53 |
watchdog: Time = Time.zero, |
75393 | 54 |
strict: Boolean = true |
55 |
): Process_Result = { |
|
72599 | 56 |
val result = |
57 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
58 |
progress_stdout = echo_if(echo, _), |
|
59 |
progress_stderr = echo_if(echo, _), |
|
60 |
watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)), |
|
61 |
strict = strict) |
|
62 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 63 |
} |
61276 | 64 |
} |
65 |
||
75393 | 66 |
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress { |
68951
a7b1fe2d30ad
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
wenzelm
parents:
68903
diff
changeset
|
67 |
override def echo(msg: String): Unit = |
71100
f31903cc57b0
clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
wenzelm
parents:
69818
diff
changeset
|
68 |
Output.writeln(msg, stdout = !stderr, include_empty = true) |
64117 | 69 |
|
68957 | 70 |
override def theory(theory: Progress.Theory): Unit = |
71 |
if (verbose) echo(theory.message) |
|
61276 | 72 |
} |
65888 | 73 |
|
75393 | 74 |
class File_Progress(path: Path, verbose: Boolean = false) extends Progress { |
65888 | 75 |
override def echo(msg: String): Unit = |
76 |
File.append(path, msg + "\n") |
|
77 |
||
68957 | 78 |
override def theory(theory: Progress.Theory): Unit = |
79 |
if (verbose) echo(theory.message) |
|
68951
a7b1fe2d30ad
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
wenzelm
parents:
68903
diff
changeset
|
80 |
|
65888 | 81 |
override def toString: String = path.toString |
82 |
} |