src/Tools/jEdit/patches/docking
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 67993 752a4e6d760c
permissions -rw-r--r--
formal update of patches -- no change of content;
wenzelm@67993
     1
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
wenzelm@67993
     2
--- 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-09 01:56:46.000000000 +0200
wenzelm@70019
     3
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2019-02-24 12:20:02.862430679 +0100
wenzelm@65329
     4
@@ -35,7 +35,7 @@
wenzelm@65329
     5
 import javax.swing.Box;
wenzelm@65329
     6
 import javax.swing.BoxLayout;
wenzelm@65329
     7
 import javax.swing.JButton;
wenzelm@65329
     8
-import javax.swing.JFrame;
wenzelm@65329
     9
+import javax.swing.JDialog;
wenzelm@65329
    10
 import javax.swing.JPopupMenu;
wenzelm@65329
    11
 import javax.swing.JSeparator;
wenzelm@65329
    12
 import javax.swing.SwingUtilities;
wenzelm@65329
    13
@@ -51,7 +51,7 @@
wenzelm@65329
    14
  * @version $Id: FloatingWindowContainer.java 24411 2016-06-19 11:02:53Z kerik-sf $
wenzelm@65329
    15
  * @since jEdit 4.0pre1
wenzelm@65329
    16
  */
wenzelm@65329
    17
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
wenzelm@65329
    18
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
wenzelm@65329
    19
 	PropertyChangeListener
wenzelm@65329
    20
 {
wenzelm@65329
    21
 	String dockableName = null;
wenzelm@65329
    22
@@ -59,6 +59,8 @@
wenzelm@65329
    23
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
wenzelm@65329
    24
 		boolean clone)
wenzelm@65329
    25
 	{
wenzelm@65329
    26
+		super(dockableWindowManager.getView());
wenzelm@65329
    27
+
wenzelm@65329
    28
 		this.dockableWindowManager = dockableWindowManager;
wenzelm@65329
    29
 
wenzelm@65329
    30
 		dockableWindowManager.addPropertyChangeListener(this);
wenzelm@65329
    31
@@ -94,7 +96,6 @@
wenzelm@65329
    32
 		pack();
wenzelm@65329
    33
 		Container parent = dockableWindowManager.getView();
wenzelm@65329
    34
 		GUIUtilities.loadGeometry(this, parent, dockableName);
wenzelm@65329
    35
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
wenzelm@65329
    36
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
wenzelm@65329
    37
 		addKeyListener(listener);
wenzelm@65329
    38
 		getContentPane().addKeyListener(listener);
wenzelm@65329
    39
@@ -161,8 +162,11 @@
wenzelm@65329
    40
 	@Override
wenzelm@65329
    41
 	public void dispose()
wenzelm@65329
    42
 	{
wenzelm@65329
    43
-		entry.container = null;
wenzelm@65329
    44
-		entry.win = null;
wenzelm@65329
    45
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
wenzelm@65329
    46
+		if (entry != null) {
wenzelm@65329
    47
+			entry.container = null;
wenzelm@65329
    48
+			entry.win = null;
wenzelm@65329
    49
+		}
wenzelm@65329
    50
 		super.dispose();
wenzelm@65329
    51
 	} //}}}
wenzelm@65329
    52