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