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