Added properties for indexing server host and port (and methods to access them).

This commit is contained in:
Eamonn Saunders 2015-04-14 18:09:32 -04:00
parent cdbce54a7b
commit a59dfb83c5

View File

@ -43,6 +43,8 @@ public final class UserPreferences {
public static final String EXTERNAL_DATABASE_PASSWORD = "ExternalDatabasePassword"; //NON-NLS
public static final String EXTERNAL_DATABASE_TYPE = "ExternalDatabaseType"; //NON-NLS
public static final String NEW_CASE_TYPE = "NewCaseType"; //NON-NLS
public static final String INDEXING_SERVER_HOST = "IndexingServerHost"; //NON-NLS
public static final String INDEXING_SERVER_PORT = "IndexingServerPort"; //NON-NLS
// Prevent instantiation.
private UserPreferences() {
@ -126,4 +128,20 @@ public final class UserPreferences {
public static void setNewCaseType(int value) {
preferences.putInt(NEW_CASE_TYPE, value);
}
public static String getIndexingServerHost() {
return preferences.get(INDEXING_SERVER_HOST, "");
}
public static void setIndexingServerHost(String hostName) {
preferences.put(INDEXING_SERVER_HOST, hostName);
}
public static int getIndexingServerPort() {
return preferences.getInt(INDEXING_SERVER_PORT, 0);
}
public static void setIndexingServerPort(int port) {
preferences.putInt(INDEXING_SERVER_PORT, port);
}
}