String getUniqueName(String name) { return names.getName(name);
String getUniqueName(JavaToken tok) { return getUniqueName(tok.getText());
    String getUniqueName(String name) {        return names.getName(name);    }