New patch 08_doubleextensions.patch, kindly backported and provided by
[debian/jabref.git] / debian / patches / 08_doubleextensions.patch
1 Description: handle double extensions better
2 Origin: upstream
3 Bug-Debian: http://bugs.debian.org/626582
4 Forwarded: not needed, it's from them :)
5 Author: Morten Omholt Alver <mortenalver@gmail.com>
6 Reviewed-by: gregor herrmann <gregoa@debian.org>
7 Last-Update: 2011-05-22
8 Applied-Upstream: yes
9
10 --- a/src/java/net/sf/jabref/gui/FileListEntryEditor.java
11 +++ b/src/java/net/sf/jabref/gui/FileListEntryEditor.java
12 @@ -198,14 +198,9 @@
13  
14              // Try to guess the file type:
15              String theLink = link.getText().trim();
16 -            int index = theLink.lastIndexOf('.');
17 -            if ((index >= 0) && (index < theLink.length()-1)) {
18 -
19 -                ExternalFileType type = Globals.prefs.getExternalFileTypeByExt
20 -                        (theLink.substring(index+1));
21 -                if (type != null)
22 -                    types.setSelectedItem(type);
23 -            }
24 +            ExternalFileType type = Globals.prefs.getExternalFileTypeForName(theLink);
25 +            if (type != null)
26 +                types.setSelectedItem(type);
27          }
28      }
29  
30 --- a/src/java/net/sf/jabref/JabRefPreferences.java
31 +++ b/src/java/net/sf/jabref/JabRefPreferences.java
32 @@ -1065,6 +1065,27 @@
33      }
34  
35      /**
36 +     * Look up the external file type registered for this filename, if any.
37 +     * @param filename The name of the file whose type to look up.
38 +     * @return The ExternalFileType registered, or null if none.
39 +     */
40 +    public ExternalFileType getExternalFileTypeForName(String filename) {
41 +        int longestFound = -1;
42 +        ExternalFileType foundType = null;
43 +        for (Iterator<ExternalFileType> iterator = externalFileTypes.iterator(); iterator.hasNext();) {
44 +            ExternalFileType type = iterator.next();
45 +            if ((type.getExtension() != null) && filename.toLowerCase().
46 +                    endsWith(type.getExtension().toLowerCase())) {
47 +                if (type.getExtension().length() > longestFound) {
48 +                    longestFound = type.getExtension().length();
49 +                    foundType = type;
50 +                }
51 +            }
52 +        }
53 +        return foundType;
54 +    }
55 +
56 +    /**
57       * Look up the external file type registered for this MIME type, if any.
58       * @param mimeType The MIME type.
59       * @return The ExternalFileType registered, or null if none. For the mime type "text/html",