# HG changeset patch
# User wenzelm
# Date 1675189622 -3600
# Node ID c0633a0da53e1e6d51ab4672aad00509f29bae6c
# Parent  e3a7d36686294fe944081b9104afcbc52557e8ad
clarified GUI events: reset everything on session context switch;

diff -r e3a7d3668629 -r c0633a0da53e src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 18:03:27 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 19:27:02 2023 +0100
@@ -48,6 +48,12 @@
       output_main :::
       (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) :::
       output_more
+
+    def reset(): State = {
+      process.cancel()
+      progress.stop()
+      State.init()
+    }
   }
 }
 
@@ -277,6 +283,7 @@
   private lazy val delay_load: Delay =
     Delay.last(PIDE.session.load_delay, gui = true) {
       for (session <- document_session.selection_value) {
+        current_state.change(_.reset())
         if (!load_document(session)) delay_load.invoke()
         else if (document_auto()) delay_auto_build.invoke()
       }
@@ -286,6 +293,7 @@
     case SelectionChanged(_) =>
       delay_load.invoke()
       delay_build.revoke()
+      delay_auto_build.revoke()
   }
 
   private val load_button =