1/*  Title:      Pure/System/progress.scala
2    Author:     Makarius
3
4Progress context for system processes.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object Progress
14{
15  def theory_message(session: String, theory: String): String =
16    if (session == "") "theory " + theory else session + ": theory " + theory
17}
18
19class Progress
20{
21  def echo(msg: String) {}
22  def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
23  def theory(session: String, theory: String) {}
24
25  def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
26  def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
27
28  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
29    Timing.timeit(message, enabled, echo(_))(e)
30
31  def stopped: Boolean = false
32  def interrupt_handler[A](e: => A): A = e
33  def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
34  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
35
36  def bash(script: String,
37    cwd: JFile = null,
38    env: Map[String, String] = Isabelle_System.settings(),
39    redirect: Boolean = false,
40    echo: Boolean = false,
41    strict: Boolean = true): Process_Result =
42  {
43    Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
44      progress_stdout = echo_if(echo, _),
45      progress_stderr = echo_if(echo, _),
46      strict = strict)
47  }
48}
49
50object No_Progress extends Progress
51
52class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
53{
54  override def echo(msg: String)
55  {
56    Output.writeln(msg, stdout = !stderr)
57  }
58
59  override def theory(session: String, theory: String): Unit =
60    if (verbose) echo(Progress.theory_message(session, theory))
61
62  @volatile private var is_stopped = false
63  override def interrupt_handler[A](e: => A): A =
64    POSIX_Interrupt.handler { is_stopped = true } { e }
65  override def stopped: Boolean =
66  {
67    if (Thread.interrupted) is_stopped = true
68    is_stopped
69  }
70}
71
72class File_Progress(path: Path, verbose: Boolean = false) extends Progress
73{
74  override def echo(msg: String): Unit =
75    File.append(path, msg + "\n")
76
77  override def theory(session: String, theory: String): Unit =
78    if (verbose) echo(Progress.theory_message(session, theory))
79
80  override def toString: String = path.toString
81}
82