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