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 |
|
61276
|
13 |
class Progress
|
|
14 |
{
|
|
15 |
def echo(msg: String) {}
|
64049
|
16 |
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
|
61276
|
17 |
def theory(session: String, theory: String) {}
|
64909
|
18 |
|
65826
|
19 |
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
|
65828
|
20 |
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
|
65826
|
21 |
|
65921
|
22 |
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
|
|
23 |
Timing.timeit(message, enabled, echo(_))(e)
|
|
24 |
|
61276
|
25 |
def stopped: Boolean = false
|
68305
|
26 |
def interrupt_handler[A](e: => A): A = e
|
67880
|
27 |
def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
|
61276
|
28 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
|
64201
|
29 |
|
|
30 |
def bash(script: String,
|
|
31 |
cwd: JFile = null,
|
|
32 |
env: Map[String, String] = Isabelle_System.settings(),
|
|
33 |
redirect: Boolean = false,
|
65930
|
34 |
echo: Boolean = false,
|
|
35 |
strict: Boolean = true): Process_Result =
|
64201
|
36 |
{
|
|
37 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
|
|
38 |
progress_stdout = echo_if(echo, _),
|
65930
|
39 |
progress_stderr = echo_if(echo, _),
|
|
40 |
strict = strict)
|
64201
|
41 |
}
|
61276
|
42 |
}
|
|
43 |
|
64909
|
44 |
object No_Progress extends Progress
|
61276
|
45 |
|
64117
|
46 |
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
|
61276
|
47 |
{
|
64117
|
48 |
override def echo(msg: String)
|
|
49 |
{
|
67178
|
50 |
Output.writeln(msg, stdout = !stderr)
|
64117
|
51 |
}
|
|
52 |
|
61276
|
53 |
override def theory(session: String, theory: String): Unit =
|
68330
|
54 |
if (verbose) {
|
|
55 |
if (session == "") echo("theory " + theory)
|
|
56 |
else echo(session + ": theory " + theory)
|
|
57 |
}
|
61276
|
58 |
|
|
59 |
@volatile private var is_stopped = false
|
68305
|
60 |
override def interrupt_handler[A](e: => A): A =
|
|
61 |
POSIX_Interrupt.handler { is_stopped = true } { e }
|
61276
|
62 |
override def stopped: Boolean =
|
|
63 |
{
|
|
64 |
if (Thread.interrupted) is_stopped = true
|
|
65 |
is_stopped
|
|
66 |
}
|
|
67 |
}
|
65888
|
68 |
|
|
69 |
class File_Progress(path: Path, verbose: Boolean = false) extends Progress
|
|
70 |
{
|
|
71 |
override def echo(msg: String): Unit =
|
|
72 |
File.append(path, msg + "\n")
|
|
73 |
|
|
74 |
override def theory(session: String, theory: String): Unit =
|
|
75 |
if (verbose) echo(session + ": theory " + theory)
|
|
76 |
|
|
77 |
override def toString: String = path.toString
|
|
78 |
}
|