# HG changeset patch
# User wenzelm
# Date 1397558716 -7200
# Node ID 272d173cd3987198a305af3710b48238080a79d4
# Parent  83777a91f5decf2830e4276a2c247a7a4e17d9de
avoid conflict of Isabelle/jEdit popups with jEdit context menu;

diff -r 83777a91f5de -r 272d173cd398 src/Pure/GUI/popup.scala
--- 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())
   }
diff -r 83777a91f5de -r 272d173cd398 src/Tools/jEdit/src/context_menu.scala
--- 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) {