# HG changeset patch
# User wenzelm
# Date 1274557681 -7200
# Node ID 28e6cd90c1ea97302f5ffce977dc24ff9ea1d37f
# Parent  2a73253b589839a9fd3908097ed8211f22e12858
generic dockable window;

diff -r 2a73253b5898 -r 28e6cd90c1ea src/Tools/jEdit/src/jedit/dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/dockable.scala	Sat May 22 21:48:01 2010 +0200
@@ -0,0 +1,40 @@
+/*  Title:      Tools/jEdit/src/jedit/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.DockableWindowManager
+
+
+class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+{
+  if (position == DockableWindowManager.FLOATING)
+    setPreferredSize(new Dimension(500, 250))
+
+  def set_content(c: Component) = add(c, BorderLayout.CENTER)
+
+  protected def init() { }
+  protected def exit() { }
+
+  override def addNotify()
+  {
+    super.addNotify()
+    init()
+  }
+
+  override def removeNotify()
+  {
+    exit()
+    super.removeNotify()
+  }
+}