# HG changeset patch # User wenzelm # Date 1677927951 -3600 # Node ID 8fc94efa954ae2874b7821e1ebcfea987cdfe62b # Parent 2d12cb7ff829fe3a4401884e4f4dff741a09fe5d clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()"; diff -r 2d12cb7ff829 -r 8fc94efa954a src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sat Mar 04 11:45:14 2023 +0100 +++ b/src/Pure/System/progress.scala Sat Mar 04 12:05:51 2023 +0100 @@ -24,8 +24,11 @@ class Progress { def echo(msg: String): Unit = {} - def echo_if(cond: Boolean, msg: String): Unit = { if (cond) echo(msg) } - def theory(theory: Progress.Theory): Unit = {} + 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 echo_warning(msg: String): Unit = echo(Output.warning_text(msg)) @@ -63,21 +66,16 @@ } } -class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress { +class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false) +extends Progress { override def echo(msg: String): Unit = Output.writeln(msg, stdout = !stderr, include_empty = true) - - override def theory(theory: Progress.Theory): Unit = - if (verbose) echo(theory.message) } -class File_Progress(path: Path, verbose: Boolean = false) extends Progress { +class File_Progress(path: Path, override val verbose: Boolean = false) extends Progress { override def echo(msg: String): Unit = File.append(path, Output.writeln_text(msg) + "\n") - override def theory(theory: Progress.Theory): Unit = - if (verbose) echo(theory.message) - override def toString: String = path.toString } @@ -129,7 +127,8 @@ abstract class Program_Progress( default_heading: String = "Running", - default_title: String = "program" + default_title: String = "program", + override val verbose: Boolean = false ) extends Progress { private var _finished_programs: List[Program_Progress.Program] = Nil private var _running_program: Option[Program_Progress.Program] = None diff -r 2d12cb7ff829 -r 8fc94efa954a src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala Sat Mar 04 11:45:14 2023 +0100 +++ b/src/Tools/VSCode/src/channel.scala Sat Mar 04 12:05:51 2023 +0100 @@ -97,11 +97,13 @@ /* progress */ - def progress(verbose: Boolean = false): Progress = + def progress(verbose: Boolean = false): Progress = { + val verbose_ = verbose new Progress { override def echo(msg: String): Unit = log_writeln(msg) override def echo_warning(msg: String): Unit = log_warning(msg) override def echo_error_message(msg: String): Unit = log_error_message(msg) - override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) + override val verbose: Boolean = verbose_ } + } } diff -r 2d12cb7ff829 -r 8fc94efa954a src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala Sat Mar 04 11:45:14 2023 +0100 +++ b/src/Tools/jEdit/src/session_build.scala Sat Mar 04 12:05:51 2023 +0100 @@ -60,7 +60,7 @@ vertical.setValue(vertical.getMaximum) } - override def theory(theory: Progress.Theory): Unit = echo(theory.message) + override def verbose: Boolean = true }