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 }