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;
     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 object Progress
    14 {
    15   def theory_message(session: String, theory: String): String =
    16     if (session == "") "theory " + theory else session + ": theory " + theory
    17 }
    18 
    19 class Progress
    20 {
    21   def echo(msg: String) {}
    22   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    23   def theory(session: String, theory: String) {}
    24   def theory_percentage(session: String, theory: String, percentage: Int) {}
    25   def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
    26 
    27   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
    28   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
    29 
    30   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
    31     Timing.timeit(message, enabled, echo(_))(e)
    32 
    33   def stopped: Boolean = false
    34   def interrupt_handler[A](e: => A): A = e
    35   def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
    36   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    37 
    38   def bash(script: String,
    39     cwd: JFile = null,
    40     env: Map[String, String] = Isabelle_System.settings(),
    41     redirect: Boolean = false,
    42     echo: Boolean = false,
    43     strict: Boolean = true): Process_Result =
    44   {
    45     Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
    46       progress_stdout = echo_if(echo, _),
    47       progress_stderr = echo_if(echo, _),
    48       strict = strict)
    49   }
    50 }
    51 
    52 object No_Progress extends Progress
    53 
    54 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
    55 {
    56   override def echo(msg: String)
    57   {
    58     Output.writeln(msg, stdout = !stderr)
    59   }
    60 
    61   override def theory(session: String, theory: String): Unit =
    62     if (verbose) echo(Progress.theory_message(session, theory))
    63 
    64   @volatile private var is_stopped = false
    65   override def interrupt_handler[A](e: => A): A =
    66     POSIX_Interrupt.handler { is_stopped = true } { e }
    67   override def stopped: Boolean =
    68   {
    69     if (Thread.interrupted) is_stopped = true
    70     is_stopped
    71   }
    72 }
    73 
    74 class File_Progress(path: Path, verbose: Boolean = false) extends Progress
    75 {
    76   override def echo(msg: String): Unit =
    77     File.append(path, msg + "\n")
    78 
    79   override def theory(session: String, theory: String): Unit =
    80     if (verbose) echo(Progress.theory_message(session, theory))
    81 
    82   override def toString: String = path.toString
    83 }