src/Tools/jEdit/src/document_dockable.scala

 
   /* document build process */
 
   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) {
         val progress = init_progress()

               res match {
                 case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
                 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)
       }
       else st
     }