Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/sorted_properties
author haftmann
Wed, 28 Jan 2015 08:29:08 +0100
changeset 59458 9de8ac92cafa
parent 58897 527bd5a7e9f8
child 59571 1081f91c0662
permissions -rw-r--r--
abstract code equation may also be default
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58897
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     1
 
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     2
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2013-07-28 19:03:53.000000000 +0200
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     3
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2014-11-04 17:48:25.000000000 +0100
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     4
 
@@ -1468,6 +1468,27 @@
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     5
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     6
 
 	//}}}
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     7
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     8
 
+	//{{{ storeProperties() method
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
     9
 
+	/**
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    10
 
+	 * Stores properties with sorted keys.
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    11
 
+	 * @param props  Given properties.
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    12
 
+	 * @param out  Output stream.
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    13
 
+	 * @param comments  Description of the property list.
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    14
 
+	 * @since jEdit 5.3
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    15
 
+	 */
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    16
 
+	public static void storeProperties(Properties props, OutputStream out, String comments)
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    17
 
+	 	throws IOException
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    18
 
+	{
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    19
 
+	   Properties sorted = new Properties() {
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    20
 
+		   @Override
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    21
 
+		   public synchronized Enumeration<Object> keys() {
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    22
 
+			   return Collections.enumeration(new TreeSet<Object>(super.keySet()));
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    23
 
+		   }
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    24
 
+	   };
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    25
 
+	   sorted.putAll(props);
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    26
 
+	   sorted.store(out, comments);
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    27
 
+	} //}}}
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    28
 
+
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    29
 
 	static VarCompressor svc = null;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    30
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    31
 
 	//{{{ VarCompressor class
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    32
 
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    33
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java	2013-07-28 19:03:53.000000000 +0200
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    34
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java	2014-11-04 17:45:54.000000000 +0100
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    35
 
@@ -77,7 +77,7 @@
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    36
 
 	void saveUserProps(OutputStream out)
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    37
 
 		throws IOException
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    38
 
 	{
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    39
 
-		user.store(out,"jEdit properties");
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    40
 
+		MiscUtilities.storeProperties(user, out, "jEdit properties");
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    41
 
 	} //}}}
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    42
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    43
 
 	//{{{ loadPluginProps() method
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    44
 
diff -ru 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    45
 
--- 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java	2013-07-28 19:03:20.000000000 +0200
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    46
 
+++ 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java	2014-11-04 17:58:09.660507580 +0100
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    47
 
@@ -32,6 +32,7 @@
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    48
 
 import java.io.InputStream;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    49
 
 import java.util.Properties;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    50
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    51
 
+import org.gjt.sp.jedit.MiscUtilities;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    52
 
 import org.gjt.sp.util.IOUtilities;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    53
 
 import org.gjt.sp.util.Log;
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    54
 
 //}}}
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    55
 
@@ -150,7 +151,7 @@
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    56
 
 			try
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    57
 
 			{
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    58
 
 				out = new BufferedOutputStream(new FileOutputStream(userKeymapFile));
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    59
 
-				props.store(out, "jEdit's keymap " + name);
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    60
 
+				MiscUtilities.storeProperties(props, out, "jEdit's keymap " + name);
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    61
 
 			}
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    62
 
 			catch (IOException e)
527bd5a7e9f8 proper button margins for Nimbus L&F;
wenzelm
parents:
diff changeset 
    63
 
 			{
isabelle