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