diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-10-29 11:50:54.062016616 +0100
@@ -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();
} //}}}