|
1 diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java |
|
2 --- 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2013-07-28 19:03:53.000000000 +0200 |
|
3 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2014-11-04 17:48:25.000000000 +0100 |
|
4 @@ -1468,6 +1468,27 @@ |
|
5 |
|
6 //}}} |
|
7 |
|
8 + //{{{ storeProperties() method |
|
9 + /** |
|
10 + * Stores properties with sorted keys. |
|
11 + * @param props Given properties. |
|
12 + * @param out Output stream. |
|
13 + * @param comments Description of the property list. |
|
14 + * @since jEdit 5.3 |
|
15 + */ |
|
16 + public static void storeProperties(Properties props, OutputStream out, String comments) |
|
17 + throws IOException |
|
18 + { |
|
19 + Properties sorted = new Properties() { |
|
20 + @Override |
|
21 + public synchronized Enumeration<Object> keys() { |
|
22 + return Collections.enumeration(new TreeSet<Object>(super.keySet())); |
|
23 + } |
|
24 + }; |
|
25 + sorted.putAll(props); |
|
26 + sorted.store(out, comments); |
|
27 + } //}}} |
|
28 + |
|
29 static VarCompressor svc = null; |
|
30 |
|
31 //{{{ VarCompressor class |
|
32 diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java |
|
33 --- 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 2013-07-28 19:03:53.000000000 +0200 |
|
34 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java 2014-11-04 17:45:54.000000000 +0100 |
|
35 @@ -77,7 +77,7 @@ |
|
36 void saveUserProps(OutputStream out) |
|
37 throws IOException |
|
38 { |
|
39 - user.store(out,"jEdit properties"); |
|
40 + MiscUtilities.storeProperties(user, out, "jEdit properties"); |
|
41 } //}}} |
|
42 |
|
43 //{{{ loadPluginProps() method |
|
44 diff -ru 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java |
|
45 --- 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 2013-07-28 19:03:20.000000000 +0200 |
|
46 +++ 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java 2014-11-04 17:58:09.660507580 +0100 |
|
47 @@ -32,6 +32,7 @@ |
|
48 import java.io.InputStream; |
|
49 import java.util.Properties; |
|
50 |
|
51 +import org.gjt.sp.jedit.MiscUtilities; |
|
52 import org.gjt.sp.util.IOUtilities; |
|
53 import org.gjt.sp.util.Log; |
|
54 //}}} |
|
55 @@ -150,7 +151,7 @@ |
|
56 try |
|
57 { |
|
58 out = new BufferedOutputStream(new FileOutputStream(userKeymapFile)); |
|
59 - props.store(out, "jEdit's keymap " + name); |
|
60 + MiscUtilities.storeProperties(props, out, "jEdit's keymap " + name); |
|
61 } |
|
62 catch (IOException e) |
|
63 { |