clarified GUI events;
authorwenzelm
Tue, 31 Jan 2023 17:35:59 +0100
changeset 77154 dd9bde3d839e
parent 77153 0bb95bcf804e
child 77155 6840013a791a
clarified GUI events;
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") {