clarified module initialization;
authorwenzelm
Mon, 19 Dec 2022 12:33:52 +0100
changeset 76704 26f939b23fdd
parent 76703 8fac11f7f0f4
child 76705 ddf5764684dd
clarified module initialization;
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") {