--- 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()