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
Sun, 11 May 2014 20:23:08 +0200
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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56936
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     1
 
diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     2
 
--- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2013-07-28 19:03:36.000000000 +0200
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     3
 
+++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2014-05-11 19:41:50.786012120 +0200
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     4
 
@@ -26,7 +26,7 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     5
 
  * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     6
 
  * @since jEdit 2.6pre3
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     7
 
  */
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     8
 
-interface DockableWindowContainer
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
     9
 
+public interface DockableWindowContainer
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    10
 
 {
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    11
 
 	void register(DockableWindowManagerImpl.Entry entry);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    12
 
 	void remove(DockableWindowManagerImpl.Entry entry);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    13
 
diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    14
 
--- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2013-07-28 19:03:38.000000000 +0200
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    15
 
+++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2014-05-11 19:32:49.710039809 +0200
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    16
 
@@ -35,7 +35,7 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    17
 
 import javax.swing.Box;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    18
 
 import javax.swing.BoxLayout;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    19
 
 import javax.swing.JButton;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    20
 
-import javax.swing.JFrame;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    21
 
+import javax.swing.JDialog;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    22
 
 import javax.swing.JPopupMenu;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    23
 
 import javax.swing.JSeparator;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    24
 
 import javax.swing.SwingUtilities;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    25
 
@@ -50,7 +50,7 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    26
 
  * @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 
    27
 
  * @since jEdit 4.0pre1
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    28
 
  */
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    29
 
-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 
    30
 
+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 
    31
 
 	PropertyChangeListener
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    32
 
 {
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    33
 
 	String dockableName = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    34
 
@@ -58,6 +58,8 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    35
 
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    36
 
 		boolean clone)
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    37
 
 	{
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    38
 
+		super(dockableWindowManager.getView());
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    39
 
+
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    40
 
 		this.dockableWindowManager = dockableWindowManager;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    41
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    42
 
 		dockableWindowManager.addPropertyChangeListener(this);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    43
 
@@ -93,7 +95,6 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    44
 
 		pack();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    45
 
 		Container parent = dockableWindowManager.getView();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    46
 
 		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 
    47
 
-		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 
    48
 
 		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 
    49
 
 		addKeyListener(listener);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    50
 
 		getContentPane().addKeyListener(listener);
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    51
 
@@ -160,8 +161,11 @@
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    52
 
 	@Override
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    53
 
 	public void dispose()
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    54
 
 	{
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    55
 
-		entry.container = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    56
 
-		entry.win = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    57
 
+		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 
    58
 
+		if (entry != null) {
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    59
 
+			entry.container = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    60
 
+			entry.win = null;
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    61
 
+		}
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    62
 
 		super.dispose();
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    63
 
 	} //}}}
6dd8866eca69 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
diff changeset 
    64
isabelle