class GrinderProperties extends Properties {

  public final synchronized GrinderProperties
    getPropertySubset(String prefix) {
    final GrinderProperties result = new GrinderProperties();

    final Enumeration<?> propertyNames = propertyNames();

    while (propertyNames.hasMoreElements()) {
      final String name = (String)propertyNames.nextElement();

      if (name.startsWith(prefix)) {
        result.setProperty(name.substring(prefix.length()),
                           getProperty(name));
      }
    }

    return result;
  }

  public  GrinderProperties();
  public  GrinderProperties(File file);

}