# HG changeset patch
# User wenzelm
# Date 1489579748 -3600
# Node ID 2307b91159bbb547dba9c0c15f59c16699978e9f
# Parent  c3d6dd17d6267253fff18ee96fbaa5f1e03d9dc4
more explicit strict vs. non-strict initialization;

diff -r c3d6dd17d626 -r 2307b91159bb src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 12:41:22 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 13:09:08 2017 +0100
@@ -61,26 +61,14 @@
 
 class Plugin extends EBPlugin
 {
-  /* early initialization */
+  /* key parts */
 
-  val options: JEdit_Options =
-  {
-    // adhoc patch of confusing message
-    val plugin_error = jEdit.getProperty("plugin-error.start-error")
-    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin:\n{0}")
-
-    val options = new JEdit_Options(Options.init())
-
-    jEdit.setProperty("plugin-error.start-error", plugin_error)
-
-    options
-  }
+  private var _options: JEdit_Options = null
+  def options: JEdit_Options = _options
 
   val completion_history = new Completion.History_Variable
   val spell_checker = new Spell_Checker_Variable
 
-  PIDE._plugin = this
-
 
   /* global changes */
 
@@ -370,9 +358,26 @@
 
   override def start()
   {
+    /* strict initialization */
+
+    // adhoc patch of confusing message
+    val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
+    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin:\n{0}")
+
+
+    Debug.DISABLE_SEARCH_DIALOG_POOL = true
+
+    _options = new JEdit_Options(Options.init())
+
+
+    jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
+
+    PIDE._plugin = this
+
+
+    /* non-strict initialization */
+
     try {
-      Debug.DISABLE_SEARCH_DIALOG_POOL = true
-
       completion_history.load()
       spell_checker.update(options.value)