src/Tools/jEdit/src/dockable.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 53787 e64389fe2d2c
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 37067
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
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
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
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    16
import org.gjt.sp.jedit.gui.DockableWindowManager
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    17
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    18
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    19
class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    20
{
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
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37066
diff changeset
    24
  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37066
diff changeset
    25
  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
37066
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    26
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    27
  protected def init() { }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    28
  protected def exit() { }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    29
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    30
  override def addNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    31
  {
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    32
    super.addNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    33
    init()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    34
  }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    35
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    36
  override def removeNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    37
  {
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    38
    exit()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    39
    super.removeNotify()
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    40
  }
28e6cd90c1ea generic dockable window;
wenzelm
parents:
diff changeset
    41
}