src/Tools/jEdit/src/popup.scala
changeset 53247 bd595338ca18
parent 53246 8d34caf5bf82
child 53250 31f956f42e8d
--- a/src/Tools/jEdit/src/popup.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/popup.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/popup.scala
     Author:     Makarius
 
-Simple popup within layered pane, based on component with given geometry.
+Popup within layered pane.
 */
 
 package isabelle.jedit
@@ -9,17 +9,24 @@
 
 import isabelle._
 
+import java.awt.{Point, Dimension}
 import javax.swing.{JLayeredPane, JComponent}
 
 
 class Popup(
   layered: JLayeredPane,
-  component: JComponent) extends javax.swing.Popup()
+  component: JComponent,
+  location: Point,
+  size: Dimension) extends javax.swing.Popup()
 {
   override def show
   {
+    component.setLocation(location)
+    component.setSize(size)
+    component.setPreferredSize(size)
     component.setOpaque(true)
     layered.add(component, JLayeredPane.POPUP_LAYER)
+    layered.moveToFront(component)
     layered.repaint(component.getBounds())
   }