Changeset 2542 in josm for trunk/src/org/openstreetmap/josm

Timestamp:

2009-11-28T23:56:56+01:00 (15 years ago)

Author:

stoecker

Message:

cleanup plugin information a bit

Location:

trunk/src/org/openstreetmap/josm

Files:

• data/Preferences.java (modified) (1 diff)
• plugins/PluginDownloader.java (modified) (2 diffs)
• plugins/PluginHandler.java (modified) (1 diff)

trunk/src/org/openstreetmap/josm/data/Preferences.java

@@ -616 +616 @@
     }
 
+    synchronized public String getCollectionAsString(final String key) {
+        String s = get(key);
+        if(s != null && s.length() != 0)
+            s = s.replaceAll("\u001e",",");
+        return s;
+    }
+
     synchronized public Collection<String> getCollection(String key, Collection<String> def) {
         String s = get(key);

trunk/src/org/openstreetmap/josm/plugins/PluginDownloader.java

@@ -95 +95 @@
     }
 
-    private final static String[] pluginSites = {"http://josm.openstreetmap.de/plugin"};
+    private final static String[] pluginSites = {"http://josm.openstreetmap.de/plugin%<?plugins=>"};
 
     public static Collection<String> getSites() {
@@ -109 +109 @@
             /* TODO: remove old site files (everything except .jar) */
             try {
+                /* replace %<x> with empty string or x=plugins (separated with comma) */
+                String pl = Main.pref.getCollectionAsString("plugins");
+                if(pl != null && pl.length() != 0)
+                    site = site.replaceAll("%<(.*)>", "$1"+pl);
+                else
+                    site = site.replaceAll("%<(.*)>", "");
                 BufferedReader r = new BufferedReader(new InputStreamReader(new URL(site).openStream(), "utf-8"));
                 new File(Main.pref.getPreferencesDir()+"plugins").mkdir();

trunk/src/org/openstreetmap/josm/plugins/PluginHandler.java

@@ -352 +352 @@
     {
         String text = "";
-        String pl = Main.pref.get("plugins");
+        String pl = Main.pref.getCollectionAsString("plugins");
         if(pl != null && pl.length() != 0) {
             text += "Plugins: "+pl+"\n";