src/Tools/jEdit/src/dockable.scala
author wenzelm
Thu May 08 00:14:06 2014 +0200 (2014-05-08)
changeset 56906 408b526911f7
parent 53787 e64389fe2d2c
child 56931 9ecf2cbfc80d
permissions -rw-r--r--
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
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@53787
    16
import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
wenzelm@37066
    17
wenzelm@37066
    18
wenzelm@53787
    19
class Dockable(view: View, position: String)
wenzelm@53787
    20
  extends JPanel(new BorderLayout) with DefaultFocusComponent
wenzelm@37066
    21
{
wenzelm@37066
    22
  if (position == DockableWindowManager.FLOATING)
wenzelm@37066
    23
    setPreferredSize(new Dimension(500, 250))
wenzelm@37066
    24
wenzelm@53787
    25
  def focusOnDefaultComponent { requestFocus }
wenzelm@53787
    26
wenzelm@37067
    27
  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
wenzelm@37067
    28
  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
wenzelm@37066
    29
wenzelm@56906
    30
  def detach_operation: Option[() => Unit] = None
wenzelm@56906
    31
wenzelm@37066
    32
  protected def init() { }
wenzelm@37066
    33
  protected def exit() { }
wenzelm@37066
    34
wenzelm@37066
    35
  override def addNotify()
wenzelm@37066
    36
  {
wenzelm@37066
    37
    super.addNotify()
wenzelm@37066
    38
    init()
wenzelm@37066
    39
  }
wenzelm@37066
    40
wenzelm@37066
    41
  override def removeNotify()
wenzelm@37066
    42
  {
wenzelm@37066
    43
    exit()
wenzelm@37066
    44
    super.removeNotify()
wenzelm@37066
    45
  }
wenzelm@37066
    46
}