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