# HG changeset patch # User wenzelm # Date 1677947789 -3600 # Node ID a8175b950173b88614d8c6f0a7498342113c75dd # Parent 7ee426daafa313a840023cf3df153925d4373422 more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress); diff -r 7ee426daafa3 -r a8175b950173 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sat Mar 04 16:45:21 2023 +0100 +++ b/src/Pure/System/progress.scala Sat Mar 04 17:36:29 2023 +0100 @@ -38,22 +38,25 @@ class Progress { def echo(message: Progress.Message) = {} - def echo(msg: String): Unit = + final def echo(msg: String): Unit = echo(Progress.Message(Progress.Kind.writeln, msg)) - def echo_warning(msg: String): Unit = + final def echo_warning(msg: String): Unit = echo(Progress.Message(Progress.Kind.warning, msg)) - def echo_error_message(msg: String): Unit = + final def echo_error_message(msg: String): Unit = echo(Progress.Message(Progress.Kind.error_message, msg)) - def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg) + final def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg) def verbose: Boolean = false def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} - def timeit[A](body: => A, message: Exn.Result[A] => String = null, enabled: Boolean = true): A = - Timing.timeit(body, message = message, enabled = enabled, output = echo) + final def timeit[A]( + body: => A, + message: Exn.Result[A] => String = null, + enabled: Boolean = true + ): A = Timing.timeit(body, message = message, enabled = enabled, output = echo) @volatile protected var is_stopped = false def stop(): Unit = { is_stopped = true } @@ -62,11 +65,11 @@ is_stopped } - def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } - def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() + final def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } + final def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() override def toString: String = if (stopped) "Progress(stopped)" else "Progress" - def bash(script: String, + final def bash(script: String, cwd: JFile = null, env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false,