clarified GUI events: reset everything on session context switch;
authorwenzelm
Tue, 31 Jan 2023 19:27:02 +0100
changeset 77157 c0633a0da53e
parent 77156 e3a7d3668629
child 77158 59a8b9a341aa
clarified GUI events: reset everything on session context switch;
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 =