src/Tools/jEdit/patches/docking
changeset 65329 4f3da52cec02
child 67992 752a4e6d760c
equal deleted inserted replaced
65328:2510b0ce28da 65329:4f3da52cec02
       
     1 diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
       
     2 --- 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-18 14:30:25.000000000 +0100
       
     3 +++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-19 19:27:45.730945687 +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