src/Pure/System/progress.scala
author wenzelm
Thu Oct 13 23:09:26 2016 +0200 (2016-10-13)
changeset 64201 c3edc64e219d
parent 64117 c2b41b073d8a
child 64909 8007f10195af
permissions -rw-r--r--
tuned;
wenzelm@61276
     1
/*  Title:      Pure/System/progress.scala
wenzelm@61276
     2
    Author:     Makarius
wenzelm@61276
     3
wenzelm@61276
     4
Progress context for system processes.
wenzelm@61276
     5
*/
wenzelm@61276
     6
wenzelm@61276
     7
package isabelle
wenzelm@61276
     8
wenzelm@61276
     9
wenzelm@64201
    10
import java.io.{File => JFile}
wenzelm@64201
    11
wenzelm@64201
    12
wenzelm@61276
    13
class Progress
wenzelm@61276
    14
{
wenzelm@61276
    15
  def echo(msg: String) {}
wenzelm@64049
    16
  def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
wenzelm@61276
    17
  def theory(session: String, theory: String) {}
wenzelm@61276
    18
  def stopped: Boolean = false
wenzelm@61276
    19
  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
wenzelm@64201
    20
wenzelm@64201
    21
  def bash(script: String,
wenzelm@64201
    22
    cwd: JFile = null,
wenzelm@64201
    23
    env: Map[String, String] = Isabelle_System.settings(),
wenzelm@64201
    24
    redirect: Boolean = false,
wenzelm@64201
    25
    echo: Boolean = false): Process_Result =
wenzelm@64201
    26
  {
wenzelm@64201
    27
    Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
wenzelm@64201
    28
      progress_stdout = echo_if(echo, _),
wenzelm@64201
    29
      progress_stderr = echo_if(echo, _))
wenzelm@64201
    30
  }
wenzelm@61276
    31
}
wenzelm@61276
    32
wenzelm@61276
    33
object Ignore_Progress extends Progress
wenzelm@61276
    34
wenzelm@64117
    35
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
wenzelm@61276
    36
{
wenzelm@64117
    37
  override def echo(msg: String)
wenzelm@64117
    38
  {
wenzelm@64117
    39
    if (stderr) Console.err.println(msg) else Console.println(msg)
wenzelm@64117
    40
  }
wenzelm@64117
    41
wenzelm@61276
    42
  override def theory(session: String, theory: String): Unit =
wenzelm@61276
    43
    if (verbose) echo(session + ": theory " + theory)
wenzelm@61276
    44
wenzelm@61276
    45
  @volatile private var is_stopped = false
wenzelm@61276
    46
  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
wenzelm@61276
    47
  override def stopped: Boolean =
wenzelm@61276
    48
  {
wenzelm@61276
    49
    if (Thread.interrupted) is_stopped = true
wenzelm@61276
    50
    is_stopped
wenzelm@61276
    51
  }
wenzelm@61276
    52
}