| 61276 |      1 | /*  Title:      Pure/System/progress.scala
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Progress context for system processes.
 | 
|  |      5 | */
 | 
|  |      6 | 
 | 
|  |      7 | package isabelle
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
| 64201 |     10 | import java.io.{File => JFile}
 | 
|  |     11 | 
 | 
|  |     12 | 
 | 
| 61276 |     13 | class Progress
 | 
|  |     14 | {
 | 
|  |     15 |   def echo(msg: String) {}
 | 
| 64049 |     16 |   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
 | 
| 61276 |     17 |   def theory(session: String, theory: String) {}
 | 
|  |     18 |   def stopped: Boolean = false
 | 
|  |     19 |   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 | 
| 64201 |     20 | 
 | 
|  |     21 |   def bash(script: String,
 | 
|  |     22 |     cwd: JFile = null,
 | 
|  |     23 |     env: Map[String, String] = Isabelle_System.settings(),
 | 
|  |     24 |     redirect: Boolean = false,
 | 
|  |     25 |     echo: Boolean = false): Process_Result =
 | 
|  |     26 |   {
 | 
|  |     27 |     Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
 | 
|  |     28 |       progress_stdout = echo_if(echo, _),
 | 
|  |     29 |       progress_stderr = echo_if(echo, _))
 | 
|  |     30 |   }
 | 
| 61276 |     31 | }
 | 
|  |     32 | 
 | 
|  |     33 | object Ignore_Progress extends Progress
 | 
|  |     34 | 
 | 
| 64117 |     35 | class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 | 
| 61276 |     36 | {
 | 
| 64117 |     37 |   override def echo(msg: String)
 | 
|  |     38 |   {
 | 
|  |     39 |     if (stderr) Console.err.println(msg) else Console.println(msg)
 | 
|  |     40 |   }
 | 
|  |     41 | 
 | 
| 61276 |     42 |   override def theory(session: String, theory: String): Unit =
 | 
|  |     43 |     if (verbose) echo(session + ": theory " + theory)
 | 
|  |     44 | 
 | 
|  |     45 |   @volatile private var is_stopped = false
 | 
|  |     46 |   def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
 | 
|  |     47 |   override def stopped: Boolean =
 | 
|  |     48 |   {
 | 
|  |     49 |     if (Thread.interrupted) is_stopped = true
 | 
|  |     50 |     is_stopped
 | 
|  |     51 |   }
 | 
|  |     52 | }
 |