--- 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
}
}