src/Pure/System/progress.scala
author wenzelm
Wed Oct 05 11:43:00 2016 +0200 (2016-10-05)
changeset 64049 ac3ed62c53c3
parent 61276 8a4bd05c1735
child 64117 c2b41b073d8a
permissions -rw-r--r--
misc tuning and clarification;
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@61276
    10
class Progress
wenzelm@61276
    11
{
wenzelm@61276
    12
  def echo(msg: String) {}
wenzelm@64049
    13
  def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
wenzelm@61276
    14
  def theory(session: String, theory: String) {}
wenzelm@61276
    15
  def stopped: Boolean = false
wenzelm@61276
    16
  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
wenzelm@61276
    17
}
wenzelm@61276
    18
wenzelm@61276
    19
object Ignore_Progress extends Progress
wenzelm@61276
    20
wenzelm@61276
    21
class Console_Progress(verbose: Boolean = false) extends Progress
wenzelm@61276
    22
{
wenzelm@61276
    23
  override def echo(msg: String) { Console.println(msg) }
wenzelm@61276
    24
  override def theory(session: String, theory: String): Unit =
wenzelm@61276
    25
    if (verbose) echo(session + ": theory " + theory)
wenzelm@61276
    26
wenzelm@61276
    27
  @volatile private var is_stopped = false
wenzelm@61276
    28
  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
wenzelm@61276
    29
  override def stopped: Boolean =
wenzelm@61276
    30
  {
wenzelm@61276
    31
    if (Thread.interrupted) is_stopped = true
wenzelm@61276
    32
    is_stopped
wenzelm@61276
    33
  }
wenzelm@61276
    34
}