deprecated prefixes for options

gistfile1.diff

diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java
index f189adf..d4bb029 100644
--- a/src/org/sosy_lab/common/configuration/OptionCollector.java
+++ b/src/org/sosy_lab/common/configuration/OptionCollector.java
@@ -188,18 +188,40 @@ public class OptionCollector {
     try {
       return Iterators.forEnumeration(classLoader.getResources(""));
     } catch (IOException e) {
-      System.err.println("Could not get recources of classloader.");
+      System.err.println("Could not get resources of classloader.");
     }
     return Collections.emptyIterator();
   }
 
+  private void collectOptions(final Class<?> c) {
+    final @Nullable Options classOption = c.getAnnotation(Options.class);
+    collectOptions(c, false, classOption);
+    if (classOption != null &&
+        !classOption.deprecatedPrefix().equals(Options.EMPTY_PREFIX)) {
+      collectOptions(c, true, classOption);
+    }
+  }
+
   /** This method collects every {@link Option} of a class.
    *
    * @param c class where to take the Option from
+   * @param useDeprecatedPrefix Use deprecated prefix, obviously.. todo
    */
-  private void collectOptions(final Class<?> c) {
+  private void collectOptions(final Class<?> c, boolean useDeprecatedPrefix,
+                              @Nullable Options clsOptions) {
     String classSource = getContentOfFile(c);
 
+    if (clsOptions != null && useDeprecatedPrefix) {
+      errorMessages.add(
+          String.format(
+              "WARNING: Using deprecated options prefix '%s' for  class '%s'," +
+                  "please update your config to use the prefix '%s'",
+              clsOptions.deprecatedPrefix(), c.getCanonicalName(),
+              clsOptions.prefix()
+          )
+      );
+    }
+
     for (final Field field : c.getDeclaredFields()) {
 
       if (field.isAnnotationPresent(Option.class)) {
@@ -350,7 +372,7 @@ public class OptionCollector {
   }
 
   /** This function returns the name of an {@link Option}.
-   * If no optionname is defined, the name of the field is returned.
+   * If no option name is defined, the name of the field is returned.
    * If a prefix is defined, it is added in front of the name.
    *
    * @param c class with the field
diff --git a/src/org/sosy_lab/common/configuration/Options.java b/src/org/sosy_lab/common/configuration/Options.java
index 33229b0..6768cc5 100644
--- a/src/org/sosy_lab/common/configuration/Options.java
+++ b/src/org/sosy_lab/common/configuration/Options.java
@@ -38,7 +38,22 @@ public @interface Options {
   String prefix() default "";
 
   /**
+   * When the prefix needs to be renamed, often it is desirable to maintain
+   * the backwards compatibility with the previous config.
+   * In that case, the previous prefix can be moved to the field
+   * {@code deprecatedPrefix}.
+   * Both normal and deprecated prefixes would work,
+   * with latter printing the deprecation warning.
+   */
+  String deprecatedPrefix() default EMPTY_PREFIX;
+
+  /**
    * An optional text, that describes the current options.
    */
   String description() default "";
+
+  /**
+   * Signal for the processor that the deprecated-prefix feature is not used.
+   */
+  String EMPTY_PREFIX = "<NO_DEPRECATION>";
 }