# HG changeset patch # User wenzelm # Date 1720690776 -7200 # Node ID 973d276e130eec4ad159abf34d93dde0f3a714fa # Parent 1638e980f73725503657d96937f20064d46dc040 clarified popup layer (not relevant yet); diff -r 1638e980f737 -r 973d276e130e src/Pure/GUI/popup.scala --- a/src/Pure/GUI/popup.scala Thu Jul 11 11:13:21 2024 +0200 +++ b/src/Pure/GUI/popup.scala Thu Jul 11 11:39:36 2024 +0200 @@ -22,7 +22,7 @@ component.setSize(size) component.setPreferredSize(size) component.setOpaque(true) - layered.add(component, JLayeredPane.DEFAULT_LAYER) + layered.add(component, JLayeredPane.POPUP_LAYER) layered.moveToFront(component) layered.repaint(component.getBounds()) }