Changeset 3930 in josm for trunk/src

Timestamp:

2011-02-24T19:12:02+01:00 (13 years ago)

Author:

bastiK

Message:

detect style type (xml or mapcss) by looking at the first non-whitespace byte in the inputstream

Location:

trunk/src/org/openstreetmap/josm/gui

Files:

• mappaint/MapPaintStyles.java (modified) (2 diffs)
• preferences/SourceEditor.java (modified) (1 diff)

trunk/src/org/openstreetmap/josm/gui/mappaint/MapPaintStyles.java

@@ -6 +6 @@
 import java.io.IOException;
 import java.io.InputStream;
+import java.io.InputStreamReader;
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -147 +148 @@
             if (entry.url.toLowerCase().endsWith(".mapcss")) {
                 return new MapCSSStyleSource(entry);
+            }
+            if (entry.url.toLowerCase().endsWith(".xml")) {
+                return new XmlStyleSource(entry);
             } else {
+                InputStreamReader reader = new InputStreamReader(in);
+                WHILE: while (true) {
+                    int c = reader.read();
+                    switch (c) {
+                        case -1:
+                            break WHILE;
+                        case ' ':
+                        case '\t':
+                        case '\n':
+                        case '\r':
+                            continue;
+                        case '<':
+                            return new XmlStyleSource(entry);
+                        default:
+                            return new MapCSSStyleSource(entry);
+                    }
+                }
+                System.err.println("Warning: Could not detect style type. Using default (xml).");
                 return new XmlStyleSource(entry);
             }

trunk/src/org/openstreetmap/josm/gui/preferences/SourceEditor.java

@@ -1175 +1175 @@
                             } else if ("shortdescription".equals(key) && last.title == null) {
                                 last.title = value;
+                            } else if ((lang + "title").equals(key) && last.title == null) {
+                                last.title = value;
+                            } else if ("title".equals(key) && last.title == null) {
+                                last.title = value;
                             } else if ("name".equals(key) && last.name == null) {
                                 last.name = value;