src/Tools/jEdit/src/dockable.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 43282 5d294220ca43
child 53787 e64389fe2d2c
permissions -rw-r--r--
more explicit indication of swing thread context;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/dockable.scala
wenzelm@37066
     2
    Author:     Makarius
wenzelm@37066
     3
wenzelm@37066
     4
Generic dockable window.
wenzelm@37066
     5
*/
wenzelm@37066
     6
wenzelm@37066
     7
package isabelle.jedit
wenzelm@37066
     8
wenzelm@37066
     9
wenzelm@37066
    10
import isabelle._
wenzelm@37066
    11
wenzelm@37066
    12
import java.awt.{Dimension, Component, BorderLayout}
wenzelm@37066
    13
import javax.swing.JPanel
wenzelm@37066
    14
wenzelm@37066
    15
import org.gjt.sp.jedit.View
wenzelm@37066
    16
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@37066
    17
wenzelm@37066
    18
wenzelm@37066
    19
class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
wenzelm@37066
    20
{
wenzelm@37066
    21
  if (position == DockableWindowManager.FLOATING)
wenzelm@37066
    22
    setPreferredSize(new Dimension(500, 250))
wenzelm@37066
    23
wenzelm@37067
    24
  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
wenzelm@37067
    25
  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
wenzelm@37066
    26
wenzelm@37066
    27
  protected def init() { }
wenzelm@37066
    28
  protected def exit() { }
wenzelm@37066
    29
wenzelm@37066
    30
  override def addNotify()
wenzelm@37066
    31
  {
wenzelm@37066
    32
    super.addNotify()
wenzelm@37066
    33
    init()
wenzelm@37066
    34
  }
wenzelm@37066
    35
wenzelm@37066
    36
  override def removeNotify()
wenzelm@37066
    37
  {
wenzelm@37066
    38
    exit()
wenzelm@37066
    39
    super.removeNotify()
wenzelm@37066
    40
  }
wenzelm@37066
    41
}