# HG changeset patch # User wenzelm # Date 1671449632 -3600 # Node ID 26f939b23fdd354172d1a45ac537a9e35b13ea88 # Parent 8fac11f7f0f40b7d0290f2c72fd7268d2126d82d clarified module initialization; diff -r 8fac11f7f0f4 -r 26f939b23fdd src/Tools/jEdit/src/main_plugin.scala --- 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") {