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() } }
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.7Bemerkung:
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
