--- 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
--- 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
--- /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)}
+
--- /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)
+ {