src/Tools/jEdit/src/dockable.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73987 fc363a3b690a
permissions -rw-r--r--
clarified formatting, for the sake of scala3;

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

Generic dockable window.
*/

package isabelle.jedit


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(): Unit = JEdit_Lib.request_focus_view(view)

  def set_content(c: Component): Unit = add(c, BorderLayout.CENTER)
  def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER)

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

  protected def init(): Unit = {}
  protected def exit(): Unit = {}

  override def addNotify(): Unit = {
    super.addNotify()
    init()
  }

  override def removeNotify(): Unit = {
    exit()
    super.removeNotify()
  }
}