# HG changeset patch
# User wenzelm
# Date 1675181827 -3600
# Node ID 4c9296390f20b5a76b7c3c9b494a5d62e91cc036
# Parent  2f43be96c713cb7faae57c993be4db45fa8a24fe
more accurate output: avoid output_main from last run;

diff -r 2f43be96c713 -r 4c9296390f20 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:08:16 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:17:07 2023 +0100
@@ -39,10 +39,10 @@
       copy(process = process, progress = progress, pending = if (reset_pending) false else pending)
 
     def output(results: Command.Results, body: XML.Body): State =
-      copy(output_results = results, output_main = body)
+      copy(output_results = results, output_main = body, output_more = Nil)
 
-    def finish(output: XML.Body): State =
-      copy(process = Future.value(()), output_more = output)
+    def finish(body: XML.Body): State =
+      copy(process = Future.value(()), output_more = body)
 
     def output_body: XML.Body =
       output_main :::
@@ -245,6 +245,7 @@
 
         progress.stop_program()
         output_process(progress)
+        progress.stop()
         finish_process(Pretty.separate(msgs))
 
         show_state()