more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
authorwenzelm
Sun May 11 20:23:08 2014 +0200 (2014-05-11)
changeset 569366dd8866eca69
parent 56935 63667a4ea7e2
child 56937 d11d11da0d90
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;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/docking
src/Tools/jEdit/src/pide_docking_framework.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/Admin/components/components.sha1	Fri May 09 23:00:18 2014 +0200
     1.2 +++ b/Admin/components/components.sha1	Sun May 11 20:23:08 2014 +0200
     1.3 @@ -41,6 +41,7 @@
     1.4  65cc13054be20d3a60474d406797c32a976d7db7  jedit_build-20130926.tar.gz
     1.5  30ca171f745adf12b65c798c660ac77f9c0f9b4b  jedit_build-20131106.tar.gz
     1.6  054c1300128f8abd0f46a3e92c756ccdb96ff2af  jedit_build-20140405.tar.gz
     1.7 +4a963665537ea66c69de4d761846541ebdbf69f2  jedit_build-20140511.tar.gz
     1.8  0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
     1.9  8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
    1.10  c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
     2.1 --- a/Admin/components/main	Fri May 09 23:00:18 2014 +0200
     2.2 +++ b/Admin/components/main	Sun May 11 20:23:08 2014 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  exec_process-1.0.3
     2.5  Haskabelle-2013
     2.6  jdk-8u5
     2.7 -jedit_build-20140405
     2.8 +jedit_build-20140511
     2.9  jfreechart-1.0.14-1
    2.10  jortho-1.0-2
    2.11  kodkodi-1.5.2
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/patches/docking	Sun May 11 20:23:08 2014 +0200
     3.3 @@ -0,0 +1,64 @@
     3.4 +diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
     3.5 +--- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2013-07-28 19:03:36.000000000 +0200
     3.6 ++++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java	2014-05-11 19:41:50.786012120 +0200
     3.7 +@@ -26,7 +26,7 @@
     3.8 +  * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
     3.9 +  * @since jEdit 2.6pre3
    3.10 +  */
    3.11 +-interface DockableWindowContainer
    3.12 ++public interface DockableWindowContainer
    3.13 + {
    3.14 + 	void register(DockableWindowManagerImpl.Entry entry);
    3.15 + 	void remove(DockableWindowManagerImpl.Entry entry);
    3.16 +diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
    3.17 +--- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2013-07-28 19:03:38.000000000 +0200
    3.18 ++++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2014-05-11 19:32:49.710039809 +0200
    3.19 +@@ -35,7 +35,7 @@
    3.20 + import javax.swing.Box;
    3.21 + import javax.swing.BoxLayout;
    3.22 + import javax.swing.JButton;
    3.23 +-import javax.swing.JFrame;
    3.24 ++import javax.swing.JDialog;
    3.25 + import javax.swing.JPopupMenu;
    3.26 + import javax.swing.JSeparator;
    3.27 + import javax.swing.SwingUtilities;
    3.28 +@@ -50,7 +50,7 @@
    3.29 +  * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $
    3.30 +  * @since jEdit 4.0pre1
    3.31 +  */
    3.32 +-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
    3.33 ++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
    3.34 + 	PropertyChangeListener
    3.35 + {
    3.36 + 	String dockableName = null;
    3.37 +@@ -58,6 +58,8 @@
    3.38 + 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
    3.39 + 		boolean clone)
    3.40 + 	{
    3.41 ++		super(dockableWindowManager.getView());
    3.42 ++
    3.43 + 		this.dockableWindowManager = dockableWindowManager;
    3.44 + 
    3.45 + 		dockableWindowManager.addPropertyChangeListener(this);
    3.46 +@@ -93,7 +95,6 @@
    3.47 + 		pack();
    3.48 + 		Container parent = dockableWindowManager.getView();
    3.49 + 		GUIUtilities.loadGeometry(this, parent, dockableName);
    3.50 +-		GUIUtilities.addSizeSaver(this, parent, dockableName);
    3.51 + 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
    3.52 + 		addKeyListener(listener);
    3.53 + 		getContentPane().addKeyListener(listener);
    3.54 +@@ -160,8 +161,11 @@
    3.55 + 	@Override
    3.56 + 	public void dispose()
    3.57 + 	{
    3.58 +-		entry.container = null;
    3.59 +-		entry.win = null;
    3.60 ++		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
    3.61 ++		if (entry != null) {
    3.62 ++			entry.container = null;
    3.63 ++			entry.win = null;
    3.64 ++		}
    3.65 + 		super.dispose();
    3.66 + 	} //}}}
    3.67 + 
     4.1 --- a/src/Tools/jEdit/src/pide_docking_framework.scala	Fri May 09 23:00:18 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/pide_docking_framework.scala	Sun May 11 20:23:08 2014 +0200
     4.3 @@ -4,16 +4,18 @@
     4.4  PIDE docking framework: "Original" with some add-ons.
     4.5  */
     4.6  
     4.7 -package org.gjt.sp.jedit.gui  // sic!
     4.8 +package isabelle.jedit
     4.9  
    4.10  
    4.11  import isabelle._
    4.12 -import isabelle.jedit._
    4.13  
    4.14  import java.awt.event.{ActionListener, ActionEvent}
    4.15  import javax.swing.{JPopupMenu, JMenuItem}
    4.16  
    4.17  import org.gjt.sp.jedit.View
    4.18 +import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
    4.19 +  DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
    4.20 +  FloatingWindowContainer, PanelWindowContainer}
    4.21  
    4.22  
    4.23  class PIDE_Docking_Framework extends DockableWindowManagerProvider
     5.1 --- a/src/Tools/jEdit/src/services.xml	Fri May 09 23:00:18 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/services.xml	Sun May 11 20:23:08 2014 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4      new isabelle.jedit.Context_Menu();
     5.5    </SERVICE>
     5.6  	<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
     5.7 -		new org.gjt.sp.jedit.gui.PIDE_Docking_Framework();
     5.8 +		new isabelle.jedit.PIDE_Docking_Framework();
     5.9  	</SERVICE>
    5.10    <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
    5.11      new isabelle.jedit.Isabelle_Encoding();