# HG changeset patch
# User wenzelm
# Date 1670254047 -3600
# Node ID 6827dd0c372319a8cb281eebadd7c84a75f5ee92
# Parent  02d07758ce4280f6f2c27dd7e5bdda171d94c8e3
clarified process: implicit load() when finished;

diff -r 02d07758ce42 -r 6827dd0c3723 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 05 16:24:29 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 05 16:27:27 2022 +0100
@@ -175,6 +175,7 @@
             current_state.change(_ => Document_Dockable.State.finish(result))
             show_state()
             show_page(output_page)
+            GUI_Thread.later { progress.load() }
           }
         st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
       }
@@ -236,18 +237,8 @@
       layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
     }, "Output from build process")
 
-  private val load_button =
-    new GUI.Button("Load") {
-      tooltip = "Load final log file"
-      override def clicked(): Unit = current_state.value.progress.load()
-    }
-
-  private val log_controls =
-    Wrap_Panel(List(load_button))
-
   private val log_page =
     new TabbedPane.Page("Log", new BorderPanel {
-      layout(log_controls) = BorderPanel.Position.North
       layout(scroll_log_area) = BorderPanel.Position.Center
     }, "Raw log of build process")