# HG changeset patch
# User wenzelm
# Date 1677930215 -3600
# Node ID 2e2b2bd6b2d2382832d9f892a9dfd60ffc57d5b1
# Parent  2d8815f98537896a44e24af9a981fcf14769f6b4
clarified signature: require just one "override def echo(message: Progress.Message): Unit";

diff -r 2d8815f98537 -r 2e2b2bd6b2d2 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Mar 04 12:16:58 2023 +0100
+++ b/src/Pure/System/progress.scala	Sat Mar 04 12:43:35 2023 +0100
@@ -12,8 +12,21 @@
 
 
 object Progress {
+  object Kind extends Enumeration { val writeln, warning, error_message = Value }
+  sealed case class Message(kind: Kind.Value, text: String) {
+    def output_text: String =
+      kind match {
+        case Kind.writeln => Output.writeln_text(text)
+        case Kind.warning => Output.warning_text(text)
+        case Kind.error_message => Output.error_message_text(text)
+      }
+
+    override def toString: String = output_text
+  }
+
   sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) {
-    def message: String = print_session + print_theory + print_percentage
+    def message: Message =
+      Message(Kind.writeln, print_session + print_theory + print_percentage)
 
     def print_session: String = if (session == "") "" else session + ": "
     def print_theory: String = "theory " + theory
@@ -23,7 +36,15 @@
 }
 
 class Progress {
-  def echo(msg: String): Unit = {}
+  def echo(message: Progress.Message) = {}
+
+  def echo(msg: String): Unit =
+    echo(Progress.Message(Progress.Kind.writeln, msg))
+  def echo_warning(msg: String): Unit =
+    echo(Progress.Message(Progress.Kind.warning, msg))
+  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)
 
   def verbose: Boolean = false
@@ -31,9 +52,6 @@
 
   def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
 
-  def echo_warning(msg: String): Unit = echo(Output.warning_text(msg))
-  def echo_error_message(msg: String): Unit = echo(Output.error_message_text(msg))
-
   def timeit[A](body: => A, message: Exn.Result[A] => String = null, enabled: Boolean = true): A =
     Timing.timeit(body, message = message, enabled = enabled, output = echo)
 
@@ -68,13 +86,13 @@
 
 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 echo(message: Progress.Message): Unit =
+    Output.output(message.output_text, stdout = !stderr, include_empty = true)
 }
 
 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 echo(message: Progress.Message): Unit =
+    File.append(path, message.output_text + "\n")
 
   override def toString: String = path.toString
 }
@@ -86,9 +104,9 @@
   class Program private[Program_Progress](heading: String, title: String) {
     private val output_buffer = new StringBuffer(256)  // synchronized
 
-    def echo(msg: String): Unit = synchronized {
+    def echo(message: Progress.Message): Unit = synchronized {
       if (output_buffer.length() > 0) output_buffer.append('\n')
-      output_buffer.append(msg)
+      output_buffer.append(message.output_text)
     }
 
     val start_time: Time = Time.now()
@@ -157,14 +175,15 @@
 
   def detect_program(s: String): Option[String]
 
-  override def echo(msg: String): Unit = synchronized {
-    detect_program(msg).map(Word.explode) match {
+  override def echo(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) =>
         stop_program()
         start_program(a, Word.implode(bs))
       case _ =>
         if (_running_program.isEmpty) start_program(default_heading, default_title)
-        _running_program.get.echo(msg)
+        _running_program.get.echo(message)
     }
   }
 }
diff -r 2d8815f98537 -r 2e2b2bd6b2d2 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 04 12:16:58 2023 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 04 12:43:35 2023 +0100
@@ -256,15 +256,18 @@
 
   class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
   extends Progress {
-    override def echo(msg: String): Unit = context.writeln(msg, more:_*)
-    override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
-    override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
+    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 theory(theory: Progress.Theory): Unit = {
       val entries: List[JSON.Object.Entry] =
         List("theory" -> theory.theory, "session" -> theory.session) :::
           (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
-      context.writeln(theory.message, entries ::: more.toList:_*)
+      context.writeln(theory.message.text, entries ::: more.toList:_*)
     }
 
     override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
diff -r 2d8815f98537 -r 2e2b2bd6b2d2 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Mar 04 12:16:58 2023 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Mar 04 12:43:35 2023 +0100
@@ -100,10 +100,12 @@
   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 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)
+        }
     }
   }
 }
diff -r 2d8815f98537 -r 2e2b2bd6b2d2 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sat Mar 04 12:16:58 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Sat Mar 04 12:43:35 2023 +0100
@@ -119,7 +119,7 @@
         }
       }
 
-    override def echo(msg: String): Unit = { super.echo(msg); delay.invoke() }
+    override def echo(message: Progress.Message): Unit = { super.echo(message); delay.invoke() }
     override def stop_program(): Unit = { super.stop_program(); delay.invoke() }
   }
 
diff -r 2d8815f98537 -r 2e2b2bd6b2d2 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Mar 04 12:16:58 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Mar 04 12:43:35 2023 +0100
@@ -53,9 +53,9 @@
     /* progress */
 
     private val progress = new Progress {
-      override def echo(msg: String): Unit =
+      override def echo(message: Progress.Message): Unit =
         GUI_Thread.later {
-          text.append(Output.writeln_text(msg) + "\n")
+          text.append(message.output_text + "\n")
           val vertical = scroll_text.peer.getVerticalScrollBar
           vertical.setValue(vertical.getMaximum)
         }