diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-16 13:41:31 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-16 13:41:31 -0400 |
commit | 801e6b84901c76dbeaebe756397909b0db1ee947 (patch) | |
tree | 1e8fed0f3b12a1cb3b9418a8bee301966d690f15 /src/options/base_options_handlers.h | |
parent | 839b8f788f1d240380ca72c6d245c62e8e47501b (diff) |
minor improvements (fixes) to did-you-mean suggestions
Diffstat (limited to 'src/options/base_options_handlers.h')
-rw-r--r-- | src/options/base_options_handlers.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 3779f75c1..15813a774 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -100,7 +100,8 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar Unreachable(); } -inline std::string suggestTags(char const* const* validTags, std::string inputTag) +inline std::string suggestTags(char const* const* validTags, std::string inputTag, + char const* const* additionalTags = NULL) { DidYouMean didYouMean; @@ -108,6 +109,11 @@ inline std::string suggestTags(char const* const* validTags, std::string inputTa for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { didYouMean.addWord(validTags[i]); } + if(additionalTags != NULL) { + for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) { + didYouMean.addWord(additionalTags[i]); + } + } return didYouMean.getMatchAsString(inputTag); } @@ -130,7 +136,7 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) !Configuration::isTraceTag(optarg.c_str())) { throw OptionException(std::string("debug tag ") + optarg + std::string(" not available.") + - suggestTags(Configuration::getDebugTags(), optarg) ); + suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) ); } } else if(! Configuration::isDebugBuild()) { throw OptionException("debug tags not available in non-debug builds"); |