# HG changeset patch
# User wenzelm
# Date 1662022452 -7200
# Node ID 97060c904a08356509927fcda1b4e3beb8f68189
# Parent  dda3c117f13ced4dfaa9f2c7578135845d049d46
tuned;

diff -r dda3c117f13c -r 97060c904a08 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Thu Sep 01 10:52:30 2022 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Thu Sep 01 10:54:12 2022 +0200
@@ -123,12 +123,6 @@
   private def cancel(): Unit =
     current_state.change { st => st.process.cancel(); st }
 
-  private def finish(result: Document_Dockable.Result): Unit = {
-    current_state.change { _ => Document_Dockable.State.finish(result) }
-    show_state()
-    show_page(output_page)
-  }
-
   private def build_document(): Unit = {
     current_state.change { st =>
       if (st.process.is_finished) {
@@ -148,7 +142,9 @@
                 case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
               }
             val result = Document_Dockable.Result(output = List(msg))
-            finish(result)
+            current_state.change(_ => Document_Dockable.State.finish(result))
+            show_state()
+            show_page(output_page)
           }
         st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
       }