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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73340
diff changeset
     1
/*  Title:      Tools/jEdit/src/dockable.scala
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     3
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     4
Generic dockable window.
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     5
*/
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     6
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73340
diff changeset
     7
package isabelle.jedit
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     8
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     9
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    10
import isabelle._
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    11
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    12
import java.awt.{Dimension, Component, BorderLayout}
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    13
import javax.swing.JPanel
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    14
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    15
import org.gjt.sp.jedit.View
53787
e64389fe2d2c focus on default component according to jEdit window management;
wenzelm
parents: 43282
diff changeset
    16
import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    17
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    18
53787
e64389fe2d2c focus on default component according to jEdit window management;
wenzelm
parents: 43282
diff changeset
    19
class Dockable(view: View, position: String)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
    20
extends JPanel(new BorderLayout) with DefaultFocusComponent {
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    21
  if (position == DockableWindowManager.FLOATING)
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    22
    setPreferredSize(new Dimension(500, 250))
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    23
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71525
diff changeset
    24
  def focusOnDefaultComponent(): Unit = JEdit_Lib.request_focus_view(view)
53787
e64389fe2d2c focus on default component according to jEdit window management;
wenzelm
parents: 43282
diff changeset
    25
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71525
diff changeset
    26
  def set_content(c: Component): Unit = add(c, BorderLayout.CENTER)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71525
diff changeset
    27
  def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER)
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    28
56906
408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents: 53787
diff changeset
    29
  def detach_operation: Option[() => Unit] = None
408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents: 53787
diff changeset
    30
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71525
diff changeset
    31
  protected def init(): Unit = {}
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71525
diff changeset
    32
  protected def exit(): Unit = {}
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    33
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
    34
  override def addNotify(): Unit = {
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    35
    super.addNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    36
    init()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    37
  }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    38
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
    39
  override def removeNotify(): Unit = {
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    40
    exit()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    41
    super.removeNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    42
  }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    43
}