src/Tools/jEdit/patches/docking
author haftmann
Sun, 06 Jun 2021 15:49:39 +0000
changeset 73816 0510c7a4256a
parent 73653 d9823224fcfe
child 81297 07f64697408e
permissions -rw-r--r--
moved more legacy to AFP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73653
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 72247
diff changeset
     1
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 72247
diff changeset
     2
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-03 05:31:01.000000000 +0200
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 72247
diff changeset
     3
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2021-05-10 11:02:05.760257760 +0200
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
     4
@@ -45,14 +45,15 @@
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
     5
  * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
     6
  * @since jEdit 4.0pre1
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
     7
  */
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
     8
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
     9
-{
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    10
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    11
 	private String dockableName;
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    12
 
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    13
 	//{{{ FloatingWindowContainer constructor
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    14
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    15
 		boolean clone)
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    16
 	{
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    17
+		super(dockableWindowManager.getView());
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    18
+
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    19
 		this.dockableWindowManager = dockableWindowManager;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    20
 
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    21
 		dockableWindowManager.addPropertyChangeListener(this);
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    22
@@ -87,7 +88,6 @@
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    23
 		pack();
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    24
 		Container parent = dockableWindowManager.getView();
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    25
 		GUIUtilities.loadGeometry(this, parent, dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    26
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    27
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    28
 		addKeyListener(listener);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    29
 		getContentPane().addKeyListener(listener);
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    30
@@ -154,8 +154,11 @@
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    31
 	@Override
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    32
 	public void dispose()
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    33
 	{
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    34
-		entry.container = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    35
-		entry.win = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    36
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    37
+		if (entry != null) {
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    38
+			entry.container = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    39
+			entry.win = null;
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    40
+		}
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents:
diff changeset
    41
 		super.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