1/* Title: Pure/System/progress.scala 2 Author: Makarius 3 4Progress context for system processes. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12 13object Progress 14{ 15 def theory_message(session: String, theory: String): String = 16 if (session == "") "theory " + theory else session + ": theory " + theory 17} 18 19class 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 25 def echo_warning(msg: String) { echo(Output.warning_text(msg)) } 26 def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } 27 28 def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = 29 Timing.timeit(message, enabled, echo(_))(e) 30 31 def stopped: Boolean = false 32 def interrupt_handler[A](e: => A): A = e 33 def expose_interrupt() { if (stopped) throw Exn.Interrupt() } 34 override def toString: String = if (stopped) "Progress(stopped)" else "Progress" 35 36 def bash(script: String, 37 cwd: JFile = null, 38 env: Map[String, String] = Isabelle_System.settings(), 39 redirect: Boolean = false, 40 echo: Boolean = false, 41 strict: Boolean = true): Process_Result = 42 { 43 Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, 44 progress_stdout = echo_if(echo, _), 45 progress_stderr = echo_if(echo, _), 46 strict = strict) 47 } 48} 49 50object No_Progress extends Progress 51 52class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress 53{ 54 override def echo(msg: String) 55 { 56 Output.writeln(msg, stdout = !stderr) 57 } 58 59 override def theory(session: String, theory: String): Unit = 60 if (verbose) echo(Progress.theory_message(session, theory)) 61 62 @volatile private var is_stopped = false 63 override def interrupt_handler[A](e: => A): A = 64 POSIX_Interrupt.handler { is_stopped = true } { e } 65 override def stopped: Boolean = 66 { 67 if (Thread.interrupted) is_stopped = true 68 is_stopped 69 } 70} 71 72class File_Progress(path: Path, verbose: Boolean = false) extends Progress 73{ 74 override def echo(msg: String): Unit = 75 File.append(path, msg + "\n") 76 77 override def theory(session: String, theory: String): Unit = 78 if (verbose) echo(Progress.theory_message(session, theory)) 79 80 override def toString: String = path.toString 81} 82