    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    }