# HG changeset patch
# User wenzelm
# Date 1677926714 -3600
# Node ID 2d12cb7ff829fe3a4401884e4f4dff741a09fe5d
# Parent  b9e01beef1c5dffe9044b0180152c28c04edc8be
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;

diff -r b9e01beef1c5 -r 2d12cb7ff829 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Fri Mar 03 20:11:08 2023 +0100
+++ b/src/Pure/System/progress.scala	Sat Mar 04 11:45:14 2023 +0100
@@ -73,7 +73,7 @@
 
 class File_Progress(path: Path, verbose: Boolean = false) extends Progress {
   override def echo(msg: String): Unit =
-    File.append(path, msg + "\n")
+    File.append(path, Output.writeln_text(msg) + "\n")
 
   override def theory(theory: Progress.Theory): Unit =
     if (verbose) echo(theory.message)
diff -r b9e01beef1c5 -r 2d12cb7ff829 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Fri Mar 03 20:11:08 2023 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Mar 04 11:45:14 2023 +0100
@@ -80,7 +80,7 @@
   /* display message */
 
   def display_message(message_type: Int, msg: String, show: Boolean): Unit =
-    write(LSP.DisplayMessage(message_type, Output.clean_yxml(msg), show))
+    write(LSP.DisplayMessage(message_type, Output.writeln_text(msg), show))
 
   def error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, true)
   def warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, true)
diff -r b9e01beef1c5 -r 2d12cb7ff829 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Fri Mar 03 20:11:08 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Mar 04 11:45:14 2023 +0100
@@ -53,9 +53,9 @@
     /* progress */
 
     private val progress = new Progress {
-      override def echo(txt: String): Unit =
+      override def echo(msg: String): Unit =
         GUI_Thread.later {
-          text.append(txt + "\n")
+          text.append(Output.writeln_text(msg) + "\n")
           val vertical = scroll_text.peer.getVerticalScrollBar
           vertical.setValue(vertical.getMaximum)
         }