001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    /**
006     * This module contains functions for decomposing filenames (Strings)
007     * into a basename and an extension.  I.e., "foo.java" -> "foo",
008     * ".java" and "bar" -> "bar", "".
009     *
010     * <p> Extensions include the '.' if present so that no extension can
011     * be distinguished from a blank one (i.e., "foo."). </p>
012     *
013     * <p> This also has the property that concatenating a filename's
014     * basename with its extension always gives the original
015     * filename. </p>
016     */
017    
018    public class Extension
019    {
020        /**
021         * Return the extension of a filename (including the ".") or "" if
022         * it has none.  The extension is defined as the substring
023         * starting with the last "." and ending at the end of the
024         * filename.
025         */
026        public static /*@ non_null @*/ String 
027                getExtension(/*@ non_null @*/ String filename) {
028            int lastDot = filename.lastIndexOf(".");
029    
030            if (lastDot == -1)
031                return "";          // no extension present...
032    
033            return filename.substring(lastDot);
034        }
035    
036        /**
037         * Return the basename of a filename -- the part of a filename
038         * that preceeds its extension (if any).  More precisely, the
039         * prefix of the filename preceeding the last "." or the entire
040         * filename if no "." is present.
041         */
042        public static /*@ non_null @*/ String 
043                getBasename(/*@ non_null @*/ String filename) {
044            int lastDot = filename.lastIndexOf(".");
045    
046            if (lastDot == -1)
047                return filename;            // no extension present...
048    
049            return filename.substring(0,lastDot);
050        }
051    
052        /**
053         * Return true iff a given filename has a particular extension.<p>
054         *
055         * It is faster to use endsWith for non-empty extensions; use this
056         * function when extension may be empty ("").<p>
057         */
058        public static boolean hasExtension(/*@ non_null @*/ String filename,
059                                           /*@ non_null @*/ String extension) {
060            if (!filename.endsWith(extension))
061                return false;
062    
063            if (extension.equals(""))
064                return filename.lastIndexOf(".") == -1;
065    
066            return true;
067        }
068    }