Ticket #5464: PropertiesDialog.java.patch

src/org/openstreetmap/josm/gui/dialogs/properties/PropertiesDialog.java

@@ -18 +18 @@
 import java.awt.event.MouseAdapter;
 import java.awt.event.MouseEvent;
 import java.net.HttpURLConnection;
+import java.net.ProxySelector;
 import java.net.URI;
 import java.net.URLEncoder;
 import java.util.ArrayList;
@@ -1060 +1061 @@
             try {
                 String base = new String(Main.pref.get("url.openstreetmap-wiki", "http://wiki.openstreetmap.org/wiki/"));
                 String l = LanguageInfo.getWikiLanguagePrefix();
-                List<URI> uris = new ArrayList<URI>();
+                final List<URI> uris = new ArrayList<URI>();
                 int row;
                 if (propertyTable.getSelectedRowCount() == 1) {
                     row = propertyTable.getSelectedRow();
@@ -1096 +1097 @@
                     uris.add(new URI(String.format("%sMap_Features", base)));
                 }
 
-                // find a page that actually exists in the wiki
-                HttpURLConnection conn;
-                for(URI u : uris) {
-                    conn = (HttpURLConnection) u.toURL().openConnection();
+                Main.worker.execute(new Runnable(){
+                    public void run() {
+                        try {
+                            // find a page that actually exists in the wiki
+                            HttpURLConnection conn;
+                            for(URI u : uris) {
+                                conn = (HttpURLConnection) u.toURL().openConnection(ProxySelector.getDefault().select(u).get(0));
 
-                    if (conn.getResponseCode() != 200) {
-                        System.out.println("INFO: " + u + " does not exist");
-                        conn.disconnect();
-                    } else {
-                        int osize = conn.getContentLength();
-                        conn.disconnect();
+                                if (conn.getResponseCode() != 200) {
+                                    System.out.println("INFO: " + u + " does not exist");
+                                    conn.disconnect();
+                                } else {
+                                    int osize = conn.getContentLength();
+                                    conn.disconnect();
 
-                        conn = (HttpURLConnection) new URI(u.toString()
-                                .replace("=", "%3D") /* do not URLencode whole string! */
-                                .replaceFirst("/wiki/", "/w/index.php?redirect=no&title=")
-                        ).toURL().openConnection();
+                                    conn = (HttpURLConnection) new URI(u.toString()
+                                            .replace("=", "%3D") /* do not URLencode whole string! */
+                                            .replaceFirst("/wiki/", "/w/index.php?redirect=no&title=")
+                                    ).toURL().openConnection();
 
-                        /* redirect pages have different content length, but retrieving a "nonredirect"
-                         *  page using index.php and the direct-link method gives slightly different
-                         *  content lengths, so we have to be fuzzy.. (this is UGLY, recode if u know better)
-                         */
-                        if (Math.abs(conn.getContentLength()-osize) > 200) {
-                            System.out.println("INFO: " + u + " is a mediawiki redirect");
-                            conn.disconnect();
-                        } else {
-                            System.out.println("INFO: browsing to " + u);
-                            conn.disconnect();
+                                    /* redirect pages have different content length, but retrieving a "nonredirect"
+                                     *  page using index.php and the direct-link method gives slightly different
+                                     *  content lengths, so we have to be fuzzy.. (this is UGLY, recode if u know better)
+                                     */
+                                    if (Math.abs(conn.getContentLength()-osize) > 200) {
+                                        System.out.println("INFO: " + u + " is a mediawiki redirect");
+                                        conn.disconnect();
+                                    } else {
+                                        System.out.println("INFO: browsing to " + u);
+                                        conn.disconnect();
 
-                            OpenBrowser.displayUrl(u.toString());
-                            break;
+                                        OpenBrowser.displayUrl(u.toString());
+                                        break;
+                                    }
+                                }
+                            }
+                        } catch (Exception e) {
+                            e.printStackTrace();
                         }
                     }
-                }
+                });
             } catch (Exception e1) {
                 e1.printStackTrace();
             }