# HG changeset patch
# User wenzelm
# Date 1399832588 -7200
# Node ID 6dd8866eca693a8f4df76b0a6f5a5df1a5befa86
# Parent  63667a4ea7e2e8d7e88cd592655343be7d740014
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;

diff -r 63667a4ea7e2 -r 6dd8866eca69 Admin/components/components.sha1
--- 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
diff -r 63667a4ea7e2 -r 6dd8866eca69 Admin/components/main
--- 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
diff -r 63667a4ea7e2 -r 6dd8866eca69 src/Tools/jEdit/patches/docking
--- /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();
+ 	} //}}}
+ 
diff -r 63667a4ea7e2 -r 6dd8866eca69 src/Tools/jEdit/src/pide_docking_framework.scala
--- 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
diff -r 63667a4ea7e2 -r 6dd8866eca69 src/Tools/jEdit/src/services.xml
--- 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();