avoid conflict of Isabelle/jEdit popups with jEdit context menu;
authorwenzelm
Tue, 15 Apr 2014 12:45:16 +0200
changeset 56588 272d173cd398
parent 56587 83777a91f5de
child 56589 71c5d1f516c0
avoid conflict of Isabelle/jEdit popups with jEdit context menu;
src/Pure/GUI/popup.scala
src/Tools/jEdit/src/context_menu.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())
   }
--- 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) {