src/Tools/jEdit/src/dockable.scala

more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);

/*  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()
  }
}