# HG changeset patch
# User wenzelm
# Date 1677965361 -3600
# Node ID 3bc49507bae55b2c714a286cea116b3161d02786
# Parent  7d13996ffeccbf4eb8bca53332355192f0bf4a4b
clarified treatment of "verbose" messages, e.g. Progress.theory();
always store messages within database, with explicit "verbose" flag: client-side will decide about output;

diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/Admin/build_release.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -260,7 +260,7 @@
           ssh.read_file(remote_tmp_tar, local_tmp_tar)
         }
         execute_tar(local_dir, "-xvf " + File.bash_path(local_tmp_tar))
-          .out_lines.sorted.foreach(progress.echo)
+          .out_lines.sorted.foreach(progress.echo(_))
       }
     }
     finally { ssh.close() }
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/General/ssh.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -208,8 +208,8 @@
         File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
           "download_file " + Bash.string(url_name) + " " + bash_path(file)
       execute(cmd_line,
-        progress_stdout = progress.echo,
-        progress_stderr = progress.echo).check
+        progress_stdout = progress.echo(_),
+        progress_stderr = progress.echo(_)).check
     }
 
     override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/System/components.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -83,8 +83,8 @@
     progress.echo("Unpacking " + archive.base)
     ssh.execute(
       "tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive),
-      progress_stdout = progress.echo,
-      progress_stderr = progress.echo).check
+      progress_stdout = progress.echo(_),
+      progress_stderr = progress.echo(_)).check
     name
   }
 
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/System/progress.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -13,7 +13,7 @@
 
 object Progress {
   object Kind extends Enumeration { val writeln, warning, error_message = Value }
-  sealed case class Message(kind: Kind.Value, text: String) {
+  sealed case class Message(kind: Kind.Value, text: String, verbose: Boolean = false) {
     def output_text: String =
       kind match {
         case Kind.writeln => Output.writeln_text(text)
@@ -26,7 +26,7 @@
 
   sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) {
     def message: Message =
-      Message(Kind.writeln, print_session + print_theory + print_percentage)
+      Message(Kind.writeln, print_session + print_theory + print_percentage, verbose = true)
 
     def print_session: String = if_proper(session, session + ": ")
     def print_theory: String = "theory " + theory
@@ -36,27 +36,28 @@
 }
 
 class Progress {
-  def echo(message: Progress.Message) = {}
+  def verbose: Boolean = false
+  final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose
+
+  def output(message: Progress.Message) = {}
 
-  final def echo(msg: String): Unit =
-    echo(Progress.Message(Progress.Kind.writeln, msg))
-  final def echo_warning(msg: String): Unit =
-    echo(Progress.Message(Progress.Kind.warning, msg))
-  final def echo_error_message(msg: String): Unit =
-    echo(Progress.Message(Progress.Kind.error_message, msg))
+  final def echo(msg: String, verbose: Boolean = false): Unit =
+    output(Progress.Message(Progress.Kind.writeln, msg, verbose = verbose))
+  final def echo_warning(msg: String, verbose: Boolean = false): Unit =
+    output(Progress.Message(Progress.Kind.warning, msg, verbose = verbose))
+  final def echo_error_message(msg: String, verbose: Boolean = false): Unit =
+    output(Progress.Message(Progress.Kind.error_message, msg, verbose = verbose))
 
   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 theory(theory: Progress.Theory): Unit = output(theory.message)
   def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
 
   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)
+  ): A = Timing.timeit(body, message = message, enabled = enabled, output = echo(_))
 
   @volatile protected var is_stopped = false
   def stop(): Unit = { is_stopped = true }
@@ -89,16 +90,18 @@
 
 class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false)
 extends Progress {
-  override def echo(message: Progress.Message): Unit =
-    Output.output(message.output_text, stdout = !stderr, include_empty = true)
+  override def output(message: Progress.Message): Unit =
+    if (do_output(message)) {
+      Output.output(message.output_text, stdout = !stderr, include_empty = true)
+    }
 
   override def toString: String = super.toString + ": console"
 }
 
 class File_Progress(path: Path, override val verbose: Boolean = false)
 extends Progress {
-  override def echo(message: Progress.Message): Unit =
-    File.append(path, message.output_text + "\n")
+  override def output(message: Progress.Message): Unit =
+    if (do_output(message)) File.append(path, message.output_text + "\n")
 
   override def toString: String = super.toString + ": " + path.toString
 }
@@ -110,7 +113,7 @@
   class Program private[Program_Progress](heading: String, title: String) {
     private val output_buffer = new StringBuffer(256)  // synchronized
 
-    def echo(message: Progress.Message): Unit = synchronized {
+    def output(message: Progress.Message): Unit = synchronized {
       if (output_buffer.length() > 0) output_buffer.append('\n')
       output_buffer.append(message.output_text)
     }
@@ -181,7 +184,7 @@
 
   def detect_program(s: String): Option[String]
 
-  override def echo(message: Progress.Message): Unit = synchronized {
+  override def output(message: Progress.Message): Unit = synchronized {
     val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else ""
     detect_program(writeln_msg).map(Word.explode) match {
       case Some(a :: bs) =>
@@ -189,7 +192,7 @@
         start_program(a, Word.implode(bs))
       case _ =>
         if (_running_program.isEmpty) start_program(default_heading, default_title)
-        _running_program.get.echo(message)
+        if (do_output(message)) _running_program.get.output(message)
     }
   }
 }
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -502,7 +502,7 @@
                 process_result.rc, build_context.uuid)))
 
         // messages
-        process_result.err_lines.foreach(progress.echo)
+        process_result.err_lines.foreach(progress.echo(_))
 
         if (process_result.ok) {
           if (verbose) {
@@ -674,7 +674,7 @@
                     }
                     if (buffer.nonEmpty) {
                       progress.echo(thy_heading)
-                      buffer.foreach(progress.echo)
+                      buffer.foreach(progress.echo(_))
                     }
                   }
               }
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -161,7 +161,7 @@
   ) {
     def echo(progress: Progress, message_serial: Long, message: Progress.Message): State =
       if (message_serial > progress_seen) {
-        progress.echo(message)
+        progress.output(message)
         copy(progress_seen = message_serial)
       }
       else {
@@ -255,9 +255,10 @@
       val serial = SQL.Column.long("serial").make_primary_key
       val kind = SQL.Column.int("kind")
       val text = SQL.Column.string("text")
+      val verbose = SQL.Column.bool("verbose")
       val uuid = Generic.uuid
 
-      val table = make_table("progress", List(serial, kind, text, uuid))
+      val table = make_table("progress", List(serial, kind, text, verbose, uuid))
     }
 
     object Sessions {
@@ -332,7 +333,8 @@
             val serial = res.long(Progress.serial)
             val kind = isabelle.Progress.Kind(res.int(Progress.kind))
             val text = res.string(Progress.text)
-            serial -> isabelle.Progress.Message(kind, text)
+            val verbose = res.bool(Progress.verbose)
+            serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
           })
         }
 
@@ -346,7 +348,8 @@
         stmt.long(1) = message_serial
         stmt.int(2) = message.kind.id
         stmt.string(3) = message.text
-        stmt.string(4) = uuid
+        stmt.bool(4) = message.verbose
+        stmt.string(5) = uuid
         stmt.execute()
       }
     }
@@ -631,18 +634,20 @@
   /* progress backed by database */
 
   object progress extends Progress {
-    override def echo(message: Progress.Message): Unit =
-      synchronized_database {
-        val serial1 = _state.serial + 1
-        _state = _state.echo(build_progress, serial1, message).copy(serial = serial1)
+    override def verbose: Boolean = build_progress.verbose
 
+    override def output(message: Progress.Message): Unit =
+      synchronized_database {
+        val state1 = _state.copy(serial = _state.serial + 1)
         for (db <- _database) {
-          Build_Process.Data.write_progress(db, serial1, message, build_context.uuid)
-          Build_Process.Data.set_serial(db, serial1)
+          Build_Process.Data.write_progress(db, state1.serial, message, build_context.uuid)
+          Build_Process.Data.set_serial(db, state1.serial)
         }
+        _state =
+          if (do_output(message)) state1.echo(build_progress, state1.serial, message)
+          else state1
       }
 
-    override def verbose: Boolean = build_progress.verbose
     override def stop(): Unit = build_progress.stop()
     override def stopped: Boolean = build_progress.stopped
   }
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -322,7 +322,7 @@
                       XML.content(Pretty.formatted(List(elem)))
                   }
                 progress.echo("FAILED to process theory " + name)
-                msgs.foreach(progress.echo_error_message)
+                msgs.foreach(progress.echo_error_message(_))
                 consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
               }
               true
diff -r 7d13996ffecc -r 3bc49507bae5 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -256,11 +256,13 @@
 
   class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
   extends Progress {
-    override def echo(message: Progress.Message): Unit =
-      message.kind match {
-        case Progress.Kind.writeln => context.writeln(message.text, more:_*)
-        case Progress.Kind.warning => context.warning(message.text, more:_*)
-        case Progress.Kind.error_message => context.error_message(message.text, more:_*)
+    override def output(message: Progress.Message): Unit =
+      if (do_output(message)) {
+        message.kind match {
+          case Progress.Kind.writeln => context.writeln(message.text, more:_*)
+          case Progress.Kind.warning => context.warning(message.text, more:_*)
+          case Progress.Kind.error_message => context.error_message(message.text, more:_*)
+        }
       }
 
     override def theory(theory: Progress.Theory): Unit = {
diff -r 7d13996ffecc -r 3bc49507bae5 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -101,11 +101,13 @@
     val verbose_ = verbose
     new Progress {
       override val verbose: Boolean = verbose_
-      override def echo(message: Progress.Message): Unit =
-        message.kind match {
-          case Progress.Kind.writeln => log_writeln(message.text)
-          case Progress.Kind.warning => log_warning(message.text)
-          case Progress.Kind.error_message => log_error_message(message.text)
+      override def output(message: Progress.Message): Unit =
+        if (do_output(message)) {
+          message.kind match {
+            case Progress.Kind.writeln => log_writeln(message.text)
+            case Progress.Kind.warning => log_warning(message.text)
+            case Progress.Kind.error_message => log_error_message(message.text)
+          }
         }
     }
   }
diff -r 7d13996ffecc -r 3bc49507bae5 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -119,7 +119,7 @@
         }
       }
 
-    override def echo(message: Progress.Message): Unit = { super.echo(message); delay.invoke() }
+    override def output(message: Progress.Message): Unit = { super.output(message); delay.invoke() }
     override def stop_program(): Unit = { super.stop_program(); delay.invoke() }
   }
 
diff -r 7d13996ffecc -r 3bc49507bae5 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Mar 04 21:41:16 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Mar 04 22:29:21 2023 +0100
@@ -53,14 +53,15 @@
     /* progress */
 
     private val progress = new Progress {
-      override def echo(message: Progress.Message): Unit =
-        GUI_Thread.later {
-          text.append(message.output_text + "\n")
-          val vertical = scroll_text.peer.getVerticalScrollBar
-          vertical.setValue(vertical.getMaximum)
+      override def verbose: Boolean = true
+      override def output(message: Progress.Message): Unit =
+        if (do_output(message)) {
+          GUI_Thread.later {
+            text.append(message.output_text + "\n")
+            val vertical = scroll_text.peer.getVerticalScrollBar
+            vertical.setValue(vertical.getMaximum)
+          }
         }
-
-      override def verbose: Boolean = true
     }