author | wenzelm |
Thu, 12 Nov 2020 16:27:31 +0100 | |
changeset 72599 | 76550282267f |
parent 72574 | d892f6d66402 |
child 72663 | e9030100f97d |
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 |
||
64201 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
13 |
object Progress |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
14 |
{ |
68957 | 15 |
sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) |
16 |
{ |
|
68987 | 17 |
def message: String = print_session + print_theory + print_percentage |
18 |
||
19 |
def print_session: String = if (session == "") "" else session + ": " |
|
20 |
def print_theory: String = "theory " + theory |
|
21 |
def print_percentage: String = |
|
22 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 23 |
} |
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
24 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
25 |
|
61276 | 26 |
class Progress |
27 |
{ |
|
28 |
def echo(msg: String) {} |
|
64049 | 29 |
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } |
68957 | 30 |
def theory(theory: Progress.Theory) {} |
69818
60d0ee8f2ddb
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents:
69817
diff
changeset
|
31 |
def nodes_status(nodes_status: Document_Status.Nodes_Status) {} |
64909 | 32 |
|
65826 | 33 |
def echo_warning(msg: String) { echo(Output.warning_text(msg)) } |
65828 | 34 |
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
71726
diff
changeset
|
35 |
def echo_document(path: Path) { echo("Document at " + path.absolute) } |
65826 | 36 |
|
65921 | 37 |
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
71601 | 38 |
Timing.timeit(message, enabled, echo)(e) |
65921 | 39 |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
40 |
@volatile protected var is_stopped = false |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
41 |
def stop { is_stopped = true } |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
42 |
def stopped: Boolean = |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
43 |
{ |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
44 |
if (Thread.interrupted) is_stopped = true |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
45 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
46 |
} |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
47 |
|
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
48 |
def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e } |
67880 | 49 |
def expose_interrupt() { if (stopped) throw Exn.Interrupt() } |
61276 | 50 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 51 |
|
52 |
def bash(script: String, |
|
53 |
cwd: JFile = null, |
|
54 |
env: Map[String, String] = Isabelle_System.settings(), |
|
55 |
redirect: Boolean = false, |
|
65930 | 56 |
echo: Boolean = false, |
72599 | 57 |
watchdog: Time = Time.zero, |
65930 | 58 |
strict: Boolean = true): Process_Result = |
64201 | 59 |
{ |
72599 | 60 |
val result = |
61 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
62 |
progress_stdout = echo_if(echo, _), |
|
63 |
progress_stderr = echo_if(echo, _), |
|
64 |
watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)), |
|
65 |
strict = strict) |
|
66 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 67 |
} |
61276 | 68 |
} |
69 |
||
64117 | 70 |
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress |
61276 | 71 |
{ |
68951
a7b1fe2d30ad
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
wenzelm
parents:
68903
diff
changeset
|
72 |
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
|
73 |
Output.writeln(msg, stdout = !stderr, include_empty = true) |
64117 | 74 |
|
68957 | 75 |
override def theory(theory: Progress.Theory): Unit = |
76 |
if (verbose) echo(theory.message) |
|
61276 | 77 |
} |
65888 | 78 |
|
79 |
class File_Progress(path: Path, verbose: Boolean = false) extends Progress |
|
80 |
{ |
|
81 |
override def echo(msg: String): Unit = |
|
82 |
File.append(path, msg + "\n") |
|
83 |
||
68957 | 84 |
override def theory(theory: Progress.Theory): Unit = |
85 |
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
|
86 |
|
65888 | 87 |
override def toString: String = path.toString |
88 |
} |