# HG changeset patch
# User wenzelm
# Date 1489520390 -3600
# Node ID 02037d14cb4260f6cdeb38b16cd2460523cfd861
# Parent  f3ba27dfaecacdff398ed61dfcb35edb61d30001
more robust early initialization;

diff -r f3ba27dfaeca -r 02037d14cb42 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 20:17:44 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 20:39:50 2017 +0100
@@ -29,14 +29,19 @@
 {
   /* plugin instance */
 
-  lazy val options = new JEdit_Options(Options.init())
+  @volatile var _plugin: Plugin = null
+
+  def plugin: Plugin =
+    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
+    else _plugin
+  def options: JEdit_Options = plugin.options
+
   val completion_history = new Completion.History_Variable
   val spell_checker = new Spell_Checker_Variable
 
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
 
-  @volatile var plugin: Plugin = null
   @volatile var session: Session = new Session(JEdit_Resources.empty)
 
   def options_changed() { if (plugin != null) plugin.options_changed() }
@@ -148,6 +153,23 @@
 
 class Plugin extends EBPlugin
 {
+  /* early initialization */
+
+  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
+  }
+  PIDE._plugin = this
+
+
   /* global changes */
 
   def options_changed()
@@ -379,7 +401,6 @@
     try {
       Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
-      PIDE.plugin = this
       PIDE.completion_history.load()
       PIDE.spell_checker.update(PIDE.options.value)