diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-02 13:55:48 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-02 13:55:48 +0000 |
commit | b5fd5b61a9f0f993703497fb1c8d678cf2d8bb01 (patch) | |
tree | 84893172fe9b731e42bf8b5b9103237c06c56252 /src/main/main.cpp | |
parent | d183c7e68eb5b191fcc9d52eaeb86ce1211ba9f7 (diff) |
Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 33 |
1 files changed, 13 insertions, 20 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index ec0a00ff8..ba5d06672 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -46,9 +46,9 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -int runCvc4(int argc, char* argv[]); -void doCommand(SmtEngine&, Command*); -void printUsage(); +static int runCvc4(int argc, char* argv[]); +static void doCommand(SmtEngine&, Command*); +static void printUsage(bool full = false); namespace CVC4 { namespace main { @@ -66,24 +66,17 @@ namespace CVC4 { } } - -// no more % chars in here without being escaped; it's used as a -// printf() format string -const string usageMessage = "\ -usage: %s [options] [input-file]\n\ -\n\ -Without an input file, or with `-', CVC4 reads from standard input.\n\ -\n\ -CVC4 options:\n"; - -void printUsage() { +static void printUsage(bool full) { stringstream ss; ss << "usage: " << options.binary_name << " [options] [input-file]" << endl << endl << "Without an input file, or with `-', CVC4 reads from standard input." << endl - << endl - << "CVC4 options:" << endl; - Options::printUsage( ss.str(), *options.out ); + << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } } /** @@ -131,7 +124,7 @@ int main(int argc, char* argv[]) { } -int runCvc4(int argc, char* argv[]) { +static int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); @@ -144,7 +137,7 @@ int runCvc4(int argc, char* argv[]) { progName = options.binary_name.c_str(); if( options.help ) { - printUsage(); + printUsage(true); exit(1); } else if( options.languageHelp ) { Options::printLanguageHelp(*options.out); @@ -357,7 +350,7 @@ int runCvc4(int argc, char* argv[]) { } /** Executes a command. Deletes the command after execution. */ -void doCommand(SmtEngine& smt, Command* cmd) { +static void doCommand(SmtEngine& smt, Command* cmd) { if( options.parseOnly ) { return; } |