src/Pure/System/progress.scala
author wenzelm
Sun May 21 20:11:12 2017 +0200 (2017-05-21)
changeset 65888 29a31cf0b4bc
parent 65828 02dd430d80c5
child 65910 5bc7e080b182
permissions -rw-r--r--
more Progress variations;
     1 /*  Title:      Pure/System/progress.scala
     2     Author:     Makarius
     3 
     4 Progress context for system processes.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 class Progress
    14 {
    15   def echo(msg: String) {}
    16   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    17   def theory(session: String, theory: String) {}
    18 
    19   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
    20   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
    21 
    22   def stopped: Boolean = false
    23   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    24 
    25   def bash(script: String,
    26     cwd: JFile = null,
    27     env: Map[String, String] = Isabelle_System.settings(),
    28     redirect: Boolean = false,
    29     echo: Boolean = false): Process_Result =
    30   {
    31     Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
    32       progress_stdout = echo_if(echo, _),
    33       progress_stderr = echo_if(echo, _))
    34   }
    35 }
    36 
    37 object No_Progress extends Progress
    38 
    39 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
    40 {
    41   override def echo(msg: String)
    42   {
    43     if (stderr) Console.err.println(msg) else Console.println(msg)
    44   }
    45 
    46   override def theory(session: String, theory: String): Unit =
    47     if (verbose) echo(session + ": theory " + theory)
    48 
    49   @volatile private var is_stopped = false
    50   def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
    51   override def stopped: Boolean =
    52   {
    53     if (Thread.interrupted) is_stopped = true
    54     is_stopped
    55   }
    56 }
    57 
    58 class File_Progress(path: Path, verbose: Boolean = false) extends Progress
    59 {
    60   override def echo(msg: String): Unit =
    61     File.append(path, msg + "\n")
    62 
    63   override def theory(session: String, theory: String): Unit =
    64     if (verbose) echo(session + ": theory " + theory)
    65 
    66   override def toString: String = path.toString
    67 }
    68 
    69 class Seq_Progress(progress1: Progress, progress2: Progress) extends Progress
    70 {
    71   override def echo(msg: String)
    72   {
    73     progress1.echo(msg)
    74     progress2.echo(msg)
    75   }
    76 
    77   override def theory(session: String, theory: String)
    78   {
    79     progress1.theory(session, theory)
    80     progress2.theory(session, theory)
    81   }
    82 }