--- a/src/Pure/GUI/popup.scala Tue Apr 15 12:34:16 2014 +0200
+++ b/src/Pure/GUI/popup.scala Tue Apr 15 12:45:16 2014 +0200
@@ -24,7 +24,7 @@
component.setSize(size)
component.setPreferredSize(size)
component.setOpaque(true)
- layered.add(component, JLayeredPane.POPUP_LAYER)
+ layered.add(component, JLayeredPane.DEFAULT_LAYER)
layered.moveToFront(component)
layered.repaint(component.getBounds())
}
--- a/src/Tools/jEdit/src/context_menu.scala Tue Apr 15 12:34:16 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala Tue Apr 15 12:45:16 2014 +0200
@@ -61,6 +61,7 @@
def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
{
+ PIDE.dismissed_popups(text_area.getView)
if (evt != null && evt.getSource == text_area.getPainter) {
val offset = text_area.xyToOffset(evt.getX, evt.getY)
if (offset >= 0) {