Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/docking
author wenzelm
Tue, 17 Apr 2018 14:48:55 +0200
changeset 67992 752a4e6d760c
parent 65329 4f3da52cec02
child 69838 4419d4d675c3
permissions -rw-r--r--
updated to jedit-5.5.0; discontinued jedit_build/contrib/jEdit-patched.tar.gz -- its content is in directory jedit_build/contrib/jedit-5.5.0-patched/jEdit;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67992
752a4e6d760c updated to jedit-5.5.0;
wenzelm
parents: 65329
diff changeset 
     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
752a4e6d760c updated to jedit-5.5.0;
wenzelm
parents: 65329
diff changeset 
     2
 
--- 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-09 01:56:46.000000000 +0200
752a4e6d760c updated to jedit-5.5.0;
wenzelm
parents: 65329
diff changeset 
     3
 
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-17 13:57:40.320348370 +0200
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     4
 
@@ -35,7 +35,7 @@
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     5
 
 import javax.swing.Box;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     6
 
 import javax.swing.BoxLayout;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     7
 
 import javax.swing.JButton;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     8
 
-import javax.swing.JFrame;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
     9
 
+import javax.swing.JDialog;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    10
 
 import javax.swing.JPopupMenu;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    11
 
 import javax.swing.JSeparator;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    12
 
 import javax.swing.SwingUtilities;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    13
 
@@ -51,7 +51,7 @@
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    14
 
  * @version $Id: FloatingWindowContainer.java 24411 2016-06-19 11:02:53Z kerik-sf $
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    15
 
  * @since jEdit 4.0pre1
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    16
 
  */
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    17
 
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    18
 
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    19
 
 	PropertyChangeListener
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    20
 
 {
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    21
 
 	String dockableName = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    22
 
@@ -59,6 +59,8 @@
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    23
 
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    24
 
 		boolean clone)
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    25
 
 	{
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    26
 
+		super(dockableWindowManager.getView());
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    27
 
+
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    28
 
 		this.dockableWindowManager = dockableWindowManager;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    29
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    30
 
 		dockableWindowManager.addPropertyChangeListener(this);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    31
 
@@ -94,7 +96,6 @@
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    32
 
 		pack();
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    33
 
 		Container parent = dockableWindowManager.getView();
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    34
 
 		GUIUtilities.loadGeometry(this, parent, dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    35
 
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    36
 
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    37
 
 		addKeyListener(listener);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    38
 
 		getContentPane().addKeyListener(listener);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    39
 
@@ -161,8 +162,11 @@
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    40
 
 	@Override
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    41
 
 	public void dispose()
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    42
 
 	{
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    43
 
-		entry.container = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    44
 
-		entry.win = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    45
 
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    46
 
+		if (entry != null) {
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    47
 
+			entry.container = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    48
 
+			entry.win = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    49
 
+		}
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    50
 
 		super.dispose();
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    51
 
 	} //}}}
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset 
    52
isabelle