--- a/src/Tools/jEdit/patches/docking Wed May 21 15:09:48 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-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 2025-05-20 15:21:47.892811800 +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);
-@@ -62,7 +63,7 @@
-
- Box caption = new Box(BoxLayout.X_AXIS);
- caption.add(menu = new RolloverButton(GUIUtilities
-- .loadIcon(jEdit.getProperty("dropdown-arrow.icon"))));
-+ .loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon"))));
- menu.addMouseListener(new MouseHandler());
- menu.setToolTipText(jEdit.getProperty("docking.menu.label"));
- Box separatorBox = new Box(BoxLayout.Y_AXIS);
-@@ -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();
- } //}}}
-