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;
--- a/Admin/components/components.sha1 Fri May 09 23:00:18 2014 +0200
+++ b/Admin/components/components.sha1 Sun May 11 20:23:08 2014 +0200
@@ -41,6 +41,7 @@
65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz
+4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
--- a/Admin/components/main Fri May 09 23:00:18 2014 +0200
+++ b/Admin/components/main Sun May 11 20:23:08 2014 +0200
@@ -4,7 +4,7 @@
exec_process-1.0.3
Haskabelle-2013
jdk-8u5
-jedit_build-20140405
+jedit_build-20140511
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/docking Sun May 11 20:23:08 2014 +0200
@@ -0,0 +1,64 @@
+diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
+--- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java 2013-07-28 19:03:36.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java 2014-05-11 19:41:50.786012120 +0200
+@@ -26,7 +26,7 @@
+ * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
+ * @since jEdit 2.6pre3
+ */
+-interface DockableWindowContainer
++public interface DockableWindowContainer
+ {
+ void register(DockableWindowManagerImpl.Entry entry);
+ void remove(DockableWindowManagerImpl.Entry entry);
+diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2013-07-28 19:03:38.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2014-05-11 19:32:49.710039809 +0200
+@@ -35,7 +35,7 @@
+ import javax.swing.Box;
+ import javax.swing.BoxLayout;
+ import javax.swing.JButton;
+-import javax.swing.JFrame;
++import javax.swing.JDialog;
+ import javax.swing.JPopupMenu;
+ import javax.swing.JSeparator;
+ import javax.swing.SwingUtilities;
+@@ -50,7 +50,7 @@
+ * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $
+ * @since jEdit 4.0pre1
+ */
+-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
+ PropertyChangeListener
+ {
+ String dockableName = null;
+@@ -58,6 +58,8 @@
+ public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
+ boolean clone)
+ {
++ super(dockableWindowManager.getView());
++
+ this.dockableWindowManager = dockableWindowManager;
+
+ dockableWindowManager.addPropertyChangeListener(this);
+@@ -93,7 +95,6 @@
+ pack();
+ Container parent = dockableWindowManager.getView();
+ GUIUtilities.loadGeometry(this, parent, dockableName);
+- GUIUtilities.addSizeSaver(this, parent, dockableName);
+ KeyListener listener = dockableWindowManager.closeListener(dockableName);
+ addKeyListener(listener);
+ getContentPane().addKeyListener(listener);
+@@ -160,8 +161,11 @@
+ @Override
+ public void dispose()
+ {
+- entry.container = null;
+- entry.win = null;
++ GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
++ if (entry != null) {
++ entry.container = null;
++ entry.win = null;
++ }
+ super.dispose();
+ } //}}}
+
--- a/src/Tools/jEdit/src/pide_docking_framework.scala Fri May 09 23:00:18 2014 +0200
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala Sun May 11 20:23:08 2014 +0200
@@ -4,16 +4,18 @@
PIDE docking framework: "Original" with some add-ons.
*/
-package org.gjt.sp.jedit.gui // sic!
+package isabelle.jedit
import isabelle._
-import isabelle.jedit._
import java.awt.event.{ActionListener, ActionEvent}
import javax.swing.{JPopupMenu, JMenuItem}
import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
+ DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
+ FloatingWindowContainer, PanelWindowContainer}
class PIDE_Docking_Framework extends DockableWindowManagerProvider
--- a/src/Tools/jEdit/src/services.xml Fri May 09 23:00:18 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Sun May 11 20:23:08 2014 +0200
@@ -6,7 +6,7 @@
new isabelle.jedit.Context_Menu();
</SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
- new org.gjt.sp.jedit.gui.PIDE_Docking_Framework();
+ new isabelle.jedit.PIDE_Docking_Framework();
</SERVICE>
<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
new isabelle.jedit.Isabelle_Encoding();