--- a/src/Tools/jEdit/src/document_dockable.scala Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Fri Nov 08 13:27:26 2024 +0100
@@ -71,8 +71,7 @@
private def show_state(): Unit = GUI_Thread.later {
val st = current_state.value
- pretty_text_area.update(Document.Snapshot.init, st.output_results,
- Pretty.separate(st.output_all))
+ pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
if (st.running) process_indicator.update("Running document build process ...", 15)
else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5)