# 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 keys() { ++ return Collections.enumeration(new TreeSet(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) + {