# 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
     }