# HG changeset patch
# User wenzelm
# Date 1415121578 -3600
# Node ID 527bd5a7e9f8f2ba04b3f8354fe7229dd447e53c
# Parent  5a2f475e2ded2c2aa90a55e7570a411b7590fbea
proper button margins for Nimbus L&F;
properties are sorted when saved;

diff -r 5a2f475e2ded -r 527bd5a7e9f8 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Nov 04 17:37:15 2014 +0100
+++ b/Admin/components/components.sha1	Tue Nov 04 18:19:38 2014 +0100
@@ -60,6 +60,7 @@
 a9d637a30f6a87a3583f265da51e63e3619cff52  jedit_build-20140722.tar.gz
 f29391c53d85715f8454e1aaa304fbccc352928f  jedit_build-20141018.tar.gz
 d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4  jedit_build-20141026.tar.gz
+f15d36abc1780875a46b6dbd4568e43b776d5db6  jedit_build-20141104.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 5a2f475e2ded -r 527bd5a7e9f8 Admin/components/main
--- a/Admin/components/main	Tue Nov 04 17:37:15 2014 +0100
+++ b/Admin/components/main	Tue Nov 04 18:19:38 2014 +0100
@@ -5,7 +5,7 @@
 exec_process-1.0.3
 Haskabelle-2014
 jdk-7u72
-jedit_build-20141026
+jedit_build-20141104
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
diff -r 5a2f475e2ded -r 527bd5a7e9f8 src/Tools/jEdit/patches/content_margin
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/content_margin	Tue Nov 04 18:19:38 2014 +0100
@@ -0,0 +1,61 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2013-07-28 19:03:36.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2014-11-04 17:51:00.000000000 +0100
+@@ -95,6 +95,7 @@
+ 			closeBox.putClientProperty("JButton.buttonType","toolbar");
+ 
+ 		closeBox.setMargin(new Insets(0,0,0,0));
++		GUIUtilities.setButtonContentMargin(closeBox, closeBox.getMargin());
+ 
+ 		closeBox.addActionListener(new ActionHandler());
+ 
+@@ -105,6 +106,7 @@
+ 			menuBtn.putClientProperty("JButton.buttonType","toolbar");
+ 
+ 		menuBtn.setMargin(new Insets(0,0,0,0));
++		GUIUtilities.setButtonContentMargin(menuBtn, menuBtn.getMargin());
+ 
+ 		menuBtn.addMouseListener(new MenuMouseHandler());
+ 
+@@ -148,6 +150,7 @@
+ 
+ 		JToggleButton button = new JToggleButton();
+ 		button.setMargin(new Insets(1,1,1,1));
++		GUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
+ 		button.setRequestFocusEnabled(false);
+ 		button.setIcon(new RotatedTextIcon(rotation,button.getFont(),
+ 			entry.shortTitle()));
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2013-07-28 19:03:53.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2014-11-04 17:52:52.000000000 +0100
+@@ -38,6 +38,7 @@
+ import org.gjt.sp.jedit.textarea.TextAreaMouseHandler;
+ import org.gjt.sp.util.Log;
+ import org.gjt.sp.util.SyntaxUtilities;
++import javax.swing.UIDefaults;
+ 
+ 
+ import java.net.URL;
+@@ -1833,6 +1834,21 @@
+ 		return (View)getComponentParent(comp,View.class);
+ 	} //}}}
+ 
++	//{{{ setButtonContentMargin() method
++	/**
++	 * Sets the content margin of a button (for Nimbus L&F).
++	 * @param button  the button to modify
++	 * @param margin  the new margin
++	 * @since jEdit 5.3
++	 */
++	public static void setButtonContentMargin(AbstractButton button, Insets margin)
++	{
++		UIDefaults defaults = new UIDefaults();
++		defaults.put("Button.contentMargins", margin);
++		defaults.put("ToggleButton.contentMargins", margin);
++		button.putClientProperty("Nimbus.Overrides", defaults);
++	} //}}}
++
+ 	//{{{ addSizeSaver() method
+ 	/**
+ 	* Adds a SizeSaver to the specified Frame. For non-Frame's use {@link #saveGeometry(Window,String)}
+
diff -r 5a2f475e2ded -r 527bd5a7e9f8 src/Tools/jEdit/patches/sorted_properties
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/sorted_properties	Tue Nov 04 18:19:38 2014 +0100
@@ -0,0 +1,63 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2013-07-28 19:03:53.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2014-11-04 17:48:25.000000000 +0100
+@@ -1468,6 +1468,27 @@
+ 
+ 	//}}}
+ 
++	//{{{ storeProperties() method
++	/**
++	 * Stores properties with sorted keys.
++	 * @param props  Given properties.
++	 * @param out  Output stream.
++	 * @param comments  Description of the property list.
++	 * @since jEdit 5.3
++	 */
++	public static void storeProperties(Properties props, OutputStream out, String comments)
++	 	throws IOException
++	{
++	   Properties sorted = new Properties() {
++		   @Override
++		   public synchronized Enumeration<Object> keys() {
++			   return Collections.enumeration(new TreeSet<Object>(super.keySet()));
++		   }
++	   };
++	   sorted.putAll(props);
++	   sorted.store(out, comments);
++	} //}}}
++
+ 	static VarCompressor svc = null;
+ 
+ 	//{{{ VarCompressor class
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java	2013-07-28 19:03:53.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java	2014-11-04 17:45:54.000000000 +0100
+@@ -77,7 +77,7 @@
+ 	void saveUserProps(OutputStream out)
+ 		throws IOException
+ 	{
+-		user.store(out,"jEdit properties");
++		MiscUtilities.storeProperties(user, out, "jEdit properties");
+ 	} //}}}
+ 
+ 	//{{{ loadPluginProps() method
+diff -ru 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java
+--- 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java	2013-07-28 19:03:20.000000000 +0200
++++ 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java	2014-11-04 17:58:09.660507580 +0100
+@@ -32,6 +32,7 @@
+ import java.io.InputStream;
+ import java.util.Properties;
+ 
++import org.gjt.sp.jedit.MiscUtilities;
+ import org.gjt.sp.util.IOUtilities;
+ import org.gjt.sp.util.Log;
+ //}}}
+@@ -150,7 +151,7 @@
+ 			try
+ 			{
+ 				out = new BufferedOutputStream(new FileOutputStream(userKeymapFile));
+-				props.store(out, "jEdit's keymap " + name);
++				MiscUtilities.storeProperties(props, out, "jEdit's keymap " + name);
+ 			}
+ 			catch (IOException e)
+ 			{