# HG changeset patch
# User wenzelm
# Date 1675182106 -3600
# Node ID 0bb95bcf804efbb3f1da04dd64af152286cf36df
# Parent  4c9296390f20b5a76b7c3c9b494a5d62e91cc036
more accurate output: avoid output_body from last run;

diff -r 4c9296390f20 -r 0bb95bcf804e src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:17:07 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:21:46 2023 +0100
@@ -231,7 +231,9 @@
     else if (document_session.is_pending) false
     else {
       run_process(reset_pending = true) { progress =>
+        output_process(progress)
         show_page(output_page)
+
         val result = Exn.capture { document_build(document_session, progress) }
         val msgs =
           result match {