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