src/Tools/jEdit/patches/docking

update to official jedit-5.6.0;

diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-08 20:13:23.565140195 +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();
 	} //}}}