org.gjt.sp.jedit.MiscUtilities.getFileExtension(String)