src/Pure/GUI/popup.scala
author wenzelm
Sun, 28 Feb 2016 21:20:51 +0100
changeset 62459 7a5d88dd8cc9
parent 56588 272d173cd398
child 64370 865b39487b5d
permissions -rw-r--r--
support only polyml-5.3.0 and polyml-5.6;

/*  Title:      Pure/GUI/popup.scala
    Module:     PIDE-GUI
    Author:     Makarius

Popup within layered pane.
*/

package isabelle


import java.awt.{Point, Dimension}
import javax.swing.{JLayeredPane, JComponent}


class Popup(
  layered: JLayeredPane,
  component: JComponent,
  location: Point,
  size: Dimension)
{
  def show
  {
    component.setLocation(location)
    component.setSize(size)
    component.setPreferredSize(size)
    component.setOpaque(true)
    layered.add(component, JLayeredPane.DEFAULT_LAYER)
    layered.moveToFront(component)
    layered.repaint(component.getBounds())
  }

  def hide
  {
    val bounds = component.getBounds()
    layered.remove(component)
    layered.repaint(bounds)
  }
}