more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
--- a/src/Tools/jEdit/src/plugin.scala Thu Nov 10 09:43:15 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Nov 10 10:20:11 2016 +0100
@@ -223,7 +223,7 @@
if (PIDE.options.bool("jedit_auto_resolve")) {
PIDE.editor.stable_tip_version() match {
case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
- case None => Nil
+ case None => delay_load.invoke(); Nil
}
}
else Nil
@@ -263,7 +263,7 @@
}
}
- lazy val delay_load =
+ private lazy val delay_load =
GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }