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;
     1 /*  Title:      Tools/jEdit/src/dockable.scala
     2     Author:     Makarius
     3 
     4 Generic dockable window.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Dimension, Component, BorderLayout}
    13 import javax.swing.JPanel
    14 
    15 import org.gjt.sp.jedit.View
    16 import org.gjt.sp.jedit.gui.DockableWindowManager
    17 
    18 
    19 class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    20 {
    21   if (position == DockableWindowManager.FLOATING)
    22     setPreferredSize(new Dimension(500, 250))
    23 
    24   def set_content(c: Component) { add(c, BorderLayout.CENTER) }
    25   def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
    26 
    27   protected def init() { }
    28   protected def exit() { }
    29 
    30   override def addNotify()
    31   {
    32     super.addNotify()
    33     init()
    34   }
    35 
    36   override def removeNotify()
    37   {
    38     exit()
    39     super.removeNotify()
    40   }
    41 }