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