more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
authorwenzelm
Thu, 10 Nov 2016 10:20:11 +0100
changeset 64478 812c22e556b9
parent 64477 8be21ca788ca
child 64479 9d643c4e9403
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
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() }