# HG changeset patch
# User wenzelm
# Date 1675182959 -3600
# Node ID dd9bde3d839e66455f7c3081f1e0f2fe9355da7e
# Parent  0bb95bcf804efbb3f1da04dd64af152286cf36df
clarified GUI events;

diff -r 0bb95bcf804e -r dd9bde3d839e src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:21:46 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:35:59 2023 +0100
@@ -282,10 +282,15 @@
     Delay.last(PIDE.session.load_delay, gui = true) {
       for (session <- document_session.selection_value) {
         if (!load_document(session)) delay_load.invoke()
+        else if (document_auto()) delay_auto_build.invoke()
       }
     }
 
-  document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() }
+  document_session.reactions += {
+    case SelectionChanged(_) =>
+      delay_load.invoke()
+      delay_build.revoke()
+  }
 
   private val load_button =
     new GUI.Button("Load") {