more accurate output: avoid output_main from last run;
authorwenzelm
Tue, 31 Jan 2023 17:17:07 +0100
changeset 77152 4c9296390f20
parent 77151 2f43be96c713
child 77153 0bb95bcf804e
more accurate output: avoid output_main from last run;
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()