--- 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") {