# HG changeset patch
# User wenzelm
# Date 1478769611 -3600
# Node ID 812c22e556b9739e667b375ddc632ae61130c822
# Parent  8be21ca788ca9d46bd159e02fdf9f9ffd759c58f
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();

diff -r 8be21ca788ca -r 812c22e556b9 src/Tools/jEdit/src/plugin.scala
--- 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() }