src/Tools/jEdit/patches/docking
author wenzelm
Sun May 11 20:23:08 2014 +0200 (2014-05-11)
changeset 56936 6dd8866eca69
child 59571 1081f91c0662
permissions -rw-r--r--
more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
prefer JDialog for FloatingWindowContainer, to keep it in front of the main window;
updated to Navigator.jar 2.5, SideKick.jar 1.6;
wenzelm@56936
     1
diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
wenzelm@56936
     2
--- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2013-07-28 19:03:36.000000000 +0200
wenzelm@56936
     3
+++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2014-05-11 19:41:50.786012120 +0200
wenzelm@56936
     4
@@ -26,7 +26,7 @@
wenzelm@56936
     5
  * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
wenzelm@56936
     6
  * @since jEdit 2.6pre3
wenzelm@56936
     7
  */
wenzelm@56936
     8
-interface DockableWindowContainer
wenzelm@56936
     9
+public interface DockableWindowContainer
wenzelm@56936
    10
 {
wenzelm@56936
    11
 	void register(DockableWindowManagerImpl.Entry entry);
wenzelm@56936
    12
 	void remove(DockableWindowManagerImpl.Entry entry);
wenzelm@56936
    13
diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
wenzelm@56936
    14
--- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2013-07-28 19:03:38.000000000 +0200
wenzelm@56936
    15
+++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2014-05-11 19:32:49.710039809 +0200
wenzelm@56936
    16
@@ -35,7 +35,7 @@
wenzelm@56936
    17
 import javax.swing.Box;
wenzelm@56936
    18
 import javax.swing.BoxLayout;
wenzelm@56936
    19
 import javax.swing.JButton;
wenzelm@56936
    20
-import javax.swing.JFrame;
wenzelm@56936
    21
+import javax.swing.JDialog;
wenzelm@56936
    22
 import javax.swing.JPopupMenu;
wenzelm@56936
    23
 import javax.swing.JSeparator;
wenzelm@56936
    24
 import javax.swing.SwingUtilities;
wenzelm@56936
    25
@@ -50,7 +50,7 @@
wenzelm@56936
    26
  * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $
wenzelm@56936
    27
  * @since jEdit 4.0pre1
wenzelm@56936
    28
  */
wenzelm@56936
    29
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
wenzelm@56936
    30
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
wenzelm@56936
    31
 	PropertyChangeListener
wenzelm@56936
    32
 {
wenzelm@56936
    33
 	String dockableName = null;
wenzelm@56936
    34
@@ -58,6 +58,8 @@
wenzelm@56936
    35
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
wenzelm@56936
    36
 		boolean clone)
wenzelm@56936
    37
 	{
wenzelm@56936
    38
+		super(dockableWindowManager.getView());
wenzelm@56936
    39
+
wenzelm@56936
    40
 		this.dockableWindowManager = dockableWindowManager;
wenzelm@56936
    41
 
wenzelm@56936
    42
 		dockableWindowManager.addPropertyChangeListener(this);
wenzelm@56936
    43
@@ -93,7 +95,6 @@
wenzelm@56936
    44
 		pack();
wenzelm@56936
    45
 		Container parent = dockableWindowManager.getView();
wenzelm@56936
    46
 		GUIUtilities.loadGeometry(this, parent, dockableName);
wenzelm@56936
    47
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
wenzelm@56936
    48
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
wenzelm@56936
    49
 		addKeyListener(listener);
wenzelm@56936
    50
 		getContentPane().addKeyListener(listener);
wenzelm@56936
    51
@@ -160,8 +161,11 @@
wenzelm@56936
    52
 	@Override
wenzelm@56936
    53
 	public void dispose()
wenzelm@56936
    54
 	{
wenzelm@56936
    55
-		entry.container = null;
wenzelm@56936
    56
-		entry.win = null;
wenzelm@56936
    57
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
wenzelm@56936
    58
+		if (entry != null) {
wenzelm@56936
    59
+			entry.container = null;
wenzelm@56936
    60
+			entry.win = null;
wenzelm@56936
    61
+		}
wenzelm@56936
    62
 		super.dispose();
wenzelm@56936
    63
 	} //}}}
wenzelm@56936
    64