src/Tools/jEdit/src-base/dockable.scala

tuned;

/*  Title:      Tools/jEdit/src-base/dockable.scala
    Author:     Makarius

Generic dockable window.
*/

package isabelle.jedit_base


import isabelle._

import java.awt.{Dimension, Component, BorderLayout}
import javax.swing.JPanel

import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}


class Dockable(view: View, position: String)
  extends JPanel(new BorderLayout) with DefaultFocusComponent
{
  if (position == DockableWindowManager.FLOATING)
    setPreferredSize(new Dimension(500, 250))

  def focusOnDefaultComponent() { JEdit_Lib.request_focus_view(view) }

  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }

  def detach_operation: Option[() => Unit] = None

  protected def init() { }
  protected def exit() { }

  override def addNotify()
  {
    super.addNotify()
    init()
  }

  override def removeNotify()
  {
    exit()
    super.removeNotify()
  }
}