# HG changeset patch
# User wenzelm
# Date 1453407165 -3600
# Node ID 027e6032977f2759d9efd2b67fa008a486b7e868
# Parent  6dfe5b12c5b2c4fe15e2540b38ba3e7a8f94c684
more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized;

diff -r 6dfe5b12c5b2 -r 027e6032977f src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Thu Jan 21 20:57:37 2016 +0100
+++ b/src/Tools/jEdit/src/context_menu.scala	Thu Jan 21 21:12:45 2016 +0100
@@ -21,22 +21,23 @@
 class Context_Menu extends DynamicContextMenuService
 {
   def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
-  {
-    PIDE.dismissed_popups(text_area.getView)
+    if (evt == null) null
+    else {
+      PIDE.dismissed_popups(text_area.getView)
 
-    val items1 =
-      if (evt != null && evt.getSource == text_area.getPainter) {
-        val offset = text_area.xyToOffset(evt.getX, evt.getY)
-        if (offset >= 0)
-          Spell_Checker.context_menu(text_area, offset) :::
-          Debugger_Dockable.context_menu(text_area, offset)
+      val items1 =
+        if (evt != null && evt.getSource == text_area.getPainter) {
+          val offset = text_area.xyToOffset(evt.getX, evt.getY)
+          if (offset >= 0)
+            Spell_Checker.context_menu(text_area, offset) :::
+            Debugger_Dockable.context_menu(text_area, offset)
+          else Nil
+        }
         else Nil
-      }
-      else Nil
+
+      val items2 = Bibtex_JEdit.context_menu(text_area)
 
-    val items2 = Bibtex_JEdit.context_menu(text_area)
-
-    val items = items1 ::: items2
-    if (items.isEmpty) null else items.toArray
+      val items = items1 ::: items2
+      if (items.isEmpty) null else items.toArray
   }
 }