src/Tools/jEdit/patches/docking

tuned;

diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2021-05-10 11:02:05.760257760 +0200
@@ -45,14 +45,15 @@
  * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
  * @since jEdit 4.0pre1
  */
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
-{
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
 	private String dockableName;
 
 	//{{{ FloatingWindowContainer constructor
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
 		boolean clone)
 	{
+		super(dockableWindowManager.getView());
+
 		this.dockableWindowManager = dockableWindowManager;
 
 		dockableWindowManager.addPropertyChangeListener(this);
@@ -87,7 +88,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);
@@ -154,8 +154,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();
 	} //}}}