author | wenzelm |
Mon, 03 Sep 2018 20:04:51 +0200 | |
changeset 68899 | b15b03c13dbb |
parent 68888 | 4fe165254e20 |
child 68903 | 58525b08eed1 |
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 |
{ |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
15 |
def theory_message(session: String, theory: String): String = |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
16 |
if (session == "") "theory " + theory else session + ": theory " + theory |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
17 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
18 |
|
61276 | 19 |
class Progress |
20 |
{ |
|
21 |
def echo(msg: String) {} |
|
64049 | 22 |
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } |
61276 | 23 |
def theory(session: String, theory: String) {} |
68899 | 24 |
def theory_percentage(session: String, theory: String, percentage: Int) {} |
68888 | 25 |
def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {} |
64909 | 26 |
|
65826 | 27 |
def echo_warning(msg: String) { echo(Output.warning_text(msg)) } |
65828 | 28 |
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } |
65826 | 29 |
|
65921 | 30 |
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
31 |
Timing.timeit(message, enabled, echo(_))(e) |
|
32 |
||
61276 | 33 |
def stopped: Boolean = false |
68305 | 34 |
def interrupt_handler[A](e: => A): A = e |
67880 | 35 |
def expose_interrupt() { if (stopped) throw Exn.Interrupt() } |
61276 | 36 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 37 |
|
38 |
def bash(script: String, |
|
39 |
cwd: JFile = null, |
|
40 |
env: Map[String, String] = Isabelle_System.settings(), |
|
41 |
redirect: Boolean = false, |
|
65930 | 42 |
echo: Boolean = false, |
43 |
strict: Boolean = true): Process_Result = |
|
64201 | 44 |
{ |
45 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
46 |
progress_stdout = echo_if(echo, _), |
|
65930 | 47 |
progress_stderr = echo_if(echo, _), |
48 |
strict = strict) |
|
64201 | 49 |
} |
61276 | 50 |
} |
51 |
||
64909 | 52 |
object No_Progress extends Progress |
61276 | 53 |
|
64117 | 54 |
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress |
61276 | 55 |
{ |
64117 | 56 |
override def echo(msg: String) |
57 |
{ |
|
67178 | 58 |
Output.writeln(msg, stdout = !stderr) |
64117 | 59 |
} |
60 |
||
61276 | 61 |
override def theory(session: String, theory: String): Unit = |
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
62 |
if (verbose) echo(Progress.theory_message(session, theory)) |
61276 | 63 |
|
64 |
@volatile private var is_stopped = false |
|
68305 | 65 |
override def interrupt_handler[A](e: => A): A = |
66 |
POSIX_Interrupt.handler { is_stopped = true } { e } |
|
61276 | 67 |
override def stopped: Boolean = |
68 |
{ |
|
69 |
if (Thread.interrupted) is_stopped = true |
|
70 |
is_stopped |
|
71 |
} |
|
72 |
} |
|
65888 | 73 |
|
74 |
class File_Progress(path: Path, verbose: Boolean = false) extends Progress |
|
75 |
{ |
|
76 |
override def echo(msg: String): Unit = |
|
77 |
File.append(path, msg + "\n") |
|
78 |
||
79 |
override def theory(session: String, theory: String): Unit = |
|
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
80 |
if (verbose) echo(Progress.theory_message(session, theory)) |
65888 | 81 |
|
82 |
override def toString: String = path.toString |
|
83 |
} |