src/Pure/System/progress.scala
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 61276 8a4bd05c1735
child 64049 ac3ed62c53c3
permissions -rw-r--r--
clarified mode of ROOT.ML files;
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
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    10
class Progress
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    11
{
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    12
  def echo(msg: String) {}
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    13
  def theory(session: String, theory: String) {}
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    14
  def stopped: Boolean = false
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    15
  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    16
}
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    17
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    18
object Ignore_Progress extends Progress
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    19
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    20
class Console_Progress(verbose: Boolean = false) extends Progress
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    21
{
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    22
  override def echo(msg: String) { Console.println(msg) }
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    23
  override def theory(session: String, theory: String): Unit =
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    24
    if (verbose) echo(session + ": theory " + theory)
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    25
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    26
  @volatile private var is_stopped = false
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    27
  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    28
  override def stopped: Boolean =
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    29
  {
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    30
    if (Thread.interrupted) is_stopped = true
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    31
    is_stopped
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    32
  }
8a4bd05c1735 clarified modules;
wenzelm
parents:
diff changeset
    33
}