--- a/src/Tools/jEdit/src/main_plugin.scala Mon Dec 19 12:22:47 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Mon Dec 19 12:33:52 2022 +0100
@@ -86,23 +86,21 @@
val spell_checker = new Spell_Checker_Variable
- /* global changes */
-
- def options_changed(): Unit = {
- session.global_options.post(Session.Global_Options(options.value))
- delay_load.invoke()
- }
-
- def deps_changed(): Unit = {
- delay_load.invoke()
- }
-
-
/* theory files */
- lazy val delay_init: Delay =
+ private lazy val delay_init: Delay =
Delay.last(PIDE.session.load_delay, gui = true) { init_models() }
+ private lazy val delay_load: Delay =
+ Delay.last(session.load_delay, gui = true) {
+ if (JEdit_Options.continuous_checking()) {
+ if (!PerspectiveManager.isPerspectiveEnabled ||
+ JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+ else if (delay_load_activated()) delay_load_body()
+ else delay_load.invoke()
+ }
+ }
+
private val delay_load_active = Synchronized(false)
private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
private def delay_load_activated(): Boolean =
@@ -148,16 +146,6 @@
else delay_load_finished()
}
- private lazy val delay_load: Delay =
- Delay.last(session.load_delay, gui = true) {
- if (JEdit_Options.continuous_checking()) {
- if (!PerspectiveManager.isPerspectiveEnabled ||
- JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
- else if (delay_load_activated()) delay_load_body()
- else delay_load.invoke()
- }
- }
-
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
@@ -165,6 +153,18 @@
File_Watcher(file_watcher_action, session.load_delay)
+ /* global changes */
+
+ def options_changed(): Unit = {
+ session.global_options.post(Session.Global_Options(options.value))
+ delay_load.invoke()
+ }
+
+ def deps_changed(): Unit = {
+ delay_load.invoke()
+ }
+
+
/* session phase */
val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit") {