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