diff --git a/src/org/sosy_lab/common/configuration/Configuration.java b/src/org/sosy_lab/common/configuration/Configuration.java index d8e935c7e..beda3382f 100644 --- a/src/org/sosy_lab/common/configuration/Configuration.java +++ b/src/org/sosy_lab/common/configuration/Configuration.java @@ -91,6 +91,8 @@ public final class Configuration { private static boolean secureMode = false; + private final Configuration parent; + /** Create a new Builder instance. */ public static ConfigurationBuilder builder() { return new ConfigurationBuilder(); @@ -116,6 +118,7 @@ public static Configuration defaultConfiguration() { new HashSet<>(0), new HashSet<>(0), null, + null, null); } @@ -131,7 +134,8 @@ public static Configuration copyWithNewPrefix(Configuration oldConfig, String ne oldConfig.unusedProperties, oldConfig.deprecatedProperties, oldConfig.printUsedOptions, - oldConfig.logger); + oldConfig.logger, + oldConfig); } /** Splitter to create string arrays. */ @@ -291,7 +295,8 @@ LogManager getLogger() { Set pUnusedProperties, Set pDeprecatedProperties, @Nullable PrintStream pPrintUsedOptions, - @Nullable LogManager pLogger) { + @Nullable LogManager pLogger, + @Nullable Configuration pParent) { checkNotNull(pProperties); checkNotNull(pSources); @@ -306,6 +311,7 @@ LogManager getLogger() { deprecatedProperties = checkNotNull(pDeprecatedProperties); printUsedOptions = pPrintUsedOptions; logger = firstNonNull(pLogger, LogManager.createNullLogManager()); + parent = pParent; } public void enableLogging(LogManager pLogger) { @@ -335,10 +341,16 @@ public String getProperty(String key) { checkNotNull(key); @Var String result = properties.get(prefix + key); unusedProperties.remove(prefix + key); + if (parent != null && result != null && result.equals(parent.getProperty(prefix + key))) { + parent.unusedProperties.remove(prefix + key); + } if (result == null && !prefix.isEmpty()) { result = properties.get(key); unusedProperties.remove(key); + if (parent != null && result != null && result.equals(parent.getProperty(key))) { + parent.unusedProperties.remove(key); + } } return result; } diff --git a/src/org/sosy_lab/common/configuration/ConfigurationBuilder.java b/src/org/sosy_lab/common/configuration/ConfigurationBuilder.java index d6f5033f8..6bde7a284 100644 --- a/src/org/sosy_lab/common/configuration/ConfigurationBuilder.java +++ b/src/org/sosy_lab/common/configuration/ConfigurationBuilder.java @@ -24,6 +24,7 @@ import static com.google.common.base.Preconditions.checkState; import com.google.common.collect.ImmutableMap; +import com.google.common.collect.Sets; import com.google.common.io.CharSource; import com.google.common.io.Resources; import com.google.errorprone.annotations.CanIgnoreReturnValue; @@ -122,8 +123,10 @@ public ConfigurationBuilder setPrefix(String newPrefix) { /** * Copy everything from an existing Configuration instance. This also means that the new - * configuration object created by this builder will share the set of unused properties with the - * configuration instance passed to this class. + * configuration object created by this builder will update the set of unused properties of the + * configuration instance passed to this class in case a property is requested. The new + * configuration will keep track of unused properties only for properties that are not present in + * the passed instance. * *

If this method is called, it has to be the first method call on this builder instance. * @@ -374,7 +377,8 @@ public Configuration build() throws InvalidConfigurationException { Set newDeprecatedProperties; if (oldConfig != null) { // share the same set of unused properties - newUnusedProperties = oldConfig.unusedProperties; + newUnusedProperties = + new HashSet<>(Sets.difference(newProperties.keySet(), oldConfig.properties.keySet())); newDeprecatedProperties = oldConfig.deprecatedProperties; } else { newUnusedProperties = new HashSet<>(newProperties.keySet()); @@ -394,7 +398,8 @@ public Configuration build() throws InvalidConfigurationException { newUnusedProperties, newDeprecatedProperties, oldConfig != null ? oldConfig.getUsedOptionsPrintStream() : null, - oldConfig != null ? oldConfig.getLogger() : null); + oldConfig != null ? oldConfig.getLogger() : null, + oldConfig); // reset builder instance so that it may be re-used properties = null; @@ -432,7 +437,8 @@ private ImmutableMap, TypeConverter> buildNewConverters( newUnusedProperties, newDeprecatedProperties, oldConfig != null ? oldConfig.getUsedOptionsPrintStream() : null, - oldConfig != null ? oldConfig.getLogger() : null); + oldConfig != null ? oldConfig.getLogger() : null, + oldConfig); // This map serves as a cache: if a single TypeConverter is used for multiple types, // we call getInstanceForNewConfiguration only once and use the new instance several times.