From d271824461acc9fd1414887308b15422962ba979 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 22 Aug 2017 16:55:44 +0200 Subject: [PATCH] prepare to initialize but not make settings known, not yet fully functioning --- src/storm/settings/SettingsManager.cpp | 15 +++++++++------ src/storm/settings/SettingsManager.h | 6 +++--- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 493ea71a2..e38c5daf2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -271,7 +271,7 @@ namespace storm { return moduleIterator->second->getPrintLengthOfLongestOption(); } - void SettingsManager::addModule(std::unique_ptr&& moduleSettings) { + void SettingsManager::addModule(std::unique_ptr&& moduleSettings, bool doRegister) { auto moduleIterator = this->modules.find(moduleSettings->getModuleName()); STORM_LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists."); @@ -281,12 +281,15 @@ namespace storm { this->modules.emplace(moduleSettings->getModuleName(), std::move(moduleSettings)); auto iterator = this->modules.find(moduleName); std::unique_ptr const& settings = iterator->second; - - // Now register the options of the module. - this->moduleOptions.emplace(moduleName, std::vector>()); - for (auto const& option : settings->getOptions()) { - this->addOption(option); + + if (doRegister) { + // Now register the options of the module. + this->moduleOptions.emplace(moduleName, std::vector>()); + for (auto const& option : settings->getOptions()) { + this->addOption(option); + } } + } void SettingsManager::addOption(std::shared_ptr