Changeset 3695 in josm

Timestamp:

2010-12-03T19:11:39+01:00 (13 years ago)

Author:

bastiK

Message:

fixed #5692 - users of imagery plugin don't see bing menu entry, because it uses old cache file from wms plugin
(Now the preference key to store the age and location of cache file contains not only the url, but the destination directory as well. Previously it could happen, that 2 plugins access the same url and try to cache it in their private plugin folder, but both plugins will share a single cache file. This used to be ok, but in this case it is no good, simply because we want a fresh download when the new plugin is installed. On top of that, in case both plugins had different caching times, the sharing wouldn't respect that either.)

File:

• trunk/src/org/openstreetmap/josm/io/MirroredInputStream.java (modified) (5 diffs)

trunk/src/org/openstreetmap/josm/io/MirroredInputStream.java

@@ -22 +22 @@
  * Mirrors a file to a local file.
  * <p>
- * The file mirrored is only downloaded if it has been more than one day since last download
+ * The file mirrored is only downloaded if it has been more than 7 days since last download
  */
 public class MirroredInputStream extends InputStream {
@@ -40 +40 @@
     }
 
+    /**
+     * Get an inputstream from a given filename, url or internal resource.
+     * @param name can be
+     *  - relative or absolute file name
+     *  - file:///SOME/FILE the same as above
+     *  - resource://SOME/FILE file from the classpath (usually in the current *.jar)
+     *  - http://... a url. It will be cached on disk.
+     * @param destDir the destination directory for the cache file. only applies for urls.
+     * @param maxTime the maximum age of the cache file (in seconds)
+     * @throws IOException when the resource with the given name could not be retrieved
+     */
     public MirroredInputStream(String name, String destDir, long maxTime) throws IOException {
         URL url;
@@ -126 +137 @@
             if (!url.getProtocol().equals("file"))
             {
-                String localPath = Main.pref.get("mirror." + url);
+                String prefKey = getPrefKey(url, destDir);
+                String localPath = Main.pref.get(prefKey);
                 if (localPath != null && localPath.length() > 0)
                 {
@@ -135 +147 @@
                     }
                 }
-                Main.pref.put("mirror." + url, null);
+                Main.pref.put(prefKey, null);
             }
         } catch (java.net.MalformedURLException e) {}
     }
 
+    /**
+     * get preference key to store the location and age of the cached file.
+     * 2 resources that point to the same url, but that are to be stored in different
+     * directories will not share a cache file.
+     */
+    private static String getPrefKey(URL url, String destDir) {
+        StringBuilder prefKey = new StringBuilder("mirror.");
+        if (destDir != null) {
+            String prefDir = Main.pref.getPreferencesDir();
+            if (destDir.startsWith(prefDir)) {
+                destDir = destDir.substring(prefDir.length());
+            }
+            prefKey.append(destDir);
+            prefKey.append(".");
+        }
+        prefKey.append(url.toString());
+        return prefKey.toString();
+    }
+
     private File checkLocal(URL url, String destDir, long maxTime) throws IOException {
-        String localPath = Main.pref.get("mirror." + url);
+        String prefKey = getPrefKey(url, destDir);
+        String localPath = Main.pref.get(prefKey);
         File file = null;
         if (localPath != null && localPath.length() > 0) {
@@ -196 +228 @@
             file = new File(destDir, localPath);
             destDirFile.renameTo(file);
-            Main.pref.put("mirror." + url, System.currentTimeMillis() + ";" + file);
+            Main.pref.put(prefKey, System.currentTimeMillis() + ";" + file);
         }