|
Feature.java
|
// FILE. . . . . /home/hak/hlt/src/hlt/osfv3/base/Feature.java // EDIT BY . . . Hassan Ait-Kaci // ON MACHINE. . Hak-Laptop // STARTED ON. . Mon Sep 02 09:13:47 2013
|
package hlt.osf.base; import java.util.HashMap;
| This is the class of ψ-term fearures as explained in the specification. |
public class Feature { /* ************************************************************************ */
| This is a global hash map associating a feature name to the unique feature bearing this name. |
private static HashMap _knownFeatures = new HashMap();
| This static method returns the feature with the given name. If the given name is null, a new feature is created and its newly created name associated to it. Therefore, this class has no public constructor. The only way to access or make a feature is by invoking the method Feature.getFeature(String name) with name identifying the feature (if null, a feature with a newly generated name is created and returned). |
public static Feature getFeature (String name) throws BadFeatureNameException
{
if (name == null)
throw new BadFeatureNameException("null feature name");
name = name.intern();
Feature feature = (Feature)_knownFeatures.get(name);
if (feature == null)
{
feature = new Feature(name);
_knownFeatures.put(feature.name(),feature);
}
return feature;
}
/* ************************************************************************ */
private Feature (String name)
{
_name = name;
}
/* ************************************************************************ */
private String _name;
public String name ()
{
return _name;
}
/* ************************************************************************ */
// It is not necessary to change the equals method: we can let it
// remain == since equals features are always uniquely identified.
// public boolean equals (Object other)
// {
// return (other instanceof Feature && _name == ((Feature)other).name());
// }
public int hashCode ()
{
return _name.hashCode();
}
/* ************************************************************************ */
| Return a string value for this feature, which is its name. |
public String toString ()
{
return name();
}
/* ************************************************************************ */
}
This file was generated on Mon Sep 09 09:17:59 PDT 2019 from file Feature.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci