src/Tools/jEdit/patches/docking
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 56936 6dd8866eca69
child 59571 1081f91c0662
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412

diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
--- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2013-07-28 19:03:36.000000000 +0200
+++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2014-05-11 19:41:50.786012120 +0200
@@ -26,7 +26,7 @@
  * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
  * @since jEdit 2.6pre3
  */
-interface DockableWindowContainer
+public interface DockableWindowContainer
 {
 	void register(DockableWindowManagerImpl.Entry entry);
 	void remove(DockableWindowManagerImpl.Entry entry);
diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2013-07-28 19:03:38.000000000 +0200
+++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2014-05-11 19:32:49.710039809 +0200
@@ -35,7 +35,7 @@
 import javax.swing.Box;
 import javax.swing.BoxLayout;
 import javax.swing.JButton;
-import javax.swing.JFrame;
+import javax.swing.JDialog;
 import javax.swing.JPopupMenu;
 import javax.swing.JSeparator;
 import javax.swing.SwingUtilities;
@@ -50,7 +50,7 @@
  * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $
  * @since jEdit 4.0pre1
  */
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
 	PropertyChangeListener
 {
 	String dockableName = null;
@@ -58,6 +58,8 @@
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
 		boolean clone)
 	{
+		super(dockableWindowManager.getView());
+
 		this.dockableWindowManager = dockableWindowManager;
 
 		dockableWindowManager.addPropertyChangeListener(this);
@@ -93,7 +95,6 @@
 		pack();
 		Container parent = dockableWindowManager.getView();
 		GUIUtilities.loadGeometry(this, parent, dockableName);
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
 		addKeyListener(listener);
 		getContentPane().addKeyListener(listener);
@@ -160,8 +161,11 @@
 	@Override
 	public void dispose()
 	{
-		entry.container = null;
-		entry.win = null;
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
+		if (entry != null) {
+			entry.container = null;
+			entry.win = null;
+		}
 		super.dispose();
 	} //}}}