optionNames.addElement(optionName);
if (!optionNames.contains(optionName)) { optionNames.addElement(optionName); }
    public void addOptionName(String optionName) {        optionNames.addElement(optionName);    }