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
Fri, 26 Jun 2015 11:44:22 +0200
changeset 60587 0318b43ee95c
parent 59571 1081f91c0662
permissions -rw-r--r--
more symbols;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 56936
diff changeset 
     1
 
diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 56936
diff changeset 
     2
 
--- 5.2.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2015-02-02 02:14:28.000000000 +0100
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 56936
diff changeset 
     3
 
+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2015-02-28 20:55:01.800035337 +0100
56936
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     4
 
@@ -35,7 +35,7 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     5
 
 import javax.swing.Box;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     6
 
 import javax.swing.BoxLayout;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     7
 
 import javax.swing.JButton;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     8
 
-import javax.swing.JFrame;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     9
 
+import javax.swing.JDialog;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    10
 
 import javax.swing.JPopupMenu;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    11
 
 import javax.swing.JSeparator;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    12
 
 import javax.swing.SwingUtilities;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    13
 
@@ -50,7 +50,7 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    14
 
  * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    15
 
  * @since jEdit 4.0pre1
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    16
 
  */
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    17
 
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    18
 
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    19
 
 	PropertyChangeListener
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    20
 
 {
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    21
 
 	String dockableName = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    22
 
@@ -58,6 +58,8 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    23
 
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    24
 
 		boolean clone)
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    25
 
 	{
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    26
 
+		super(dockableWindowManager.getView());
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    27
 
+
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    28
 
 		this.dockableWindowManager = dockableWindowManager;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    29
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    30
 
 		dockableWindowManager.addPropertyChangeListener(this);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    31
 
@@ -93,7 +95,6 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    32
 
 		pack();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    33
 
 		Container parent = dockableWindowManager.getView();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    34
 
 		GUIUtilities.loadGeometry(this, parent, dockableName);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    35
 
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    36
 
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    37
 
 		addKeyListener(listener);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    38
 
 		getContentPane().addKeyListener(listener);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    39
 
@@ -160,8 +161,11 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    40
 
 	@Override
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    41
 
 	public void dispose()
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    42
 
 	{
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    43
 
-		entry.container = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    44
 
-		entry.win = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    45
 
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    46
 
+		if (entry != null) {
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    47
 
+			entry.container = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    48
 
+			entry.win = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    49
 
+		}
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    50
 
 		super.dispose();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    51
 
 	} //}}}
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    52
isabelle