diff options
author | lianah <lianahady@gmail.com> | 2013-03-21 19:26:49 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-21 19:26:49 -0400 |
commit | c728dee765f0d07b8743fcbb452585202f3c9c96 (patch) | |
tree | a72300275c5f641c97420302df6a7657ad4307e7 /src/expr | |
parent | ff8572914d73449b26edba214ad134c596196e32 (diff) | |
parent | 2a2c5102e10a8b3f1091bc50916fda5e766b5d4a (diff) |
Merge branch 'master' into bv-core
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 7 | ||||
-rw-r--r-- | src/expr/command.h | 16 |
2 files changed, 21 insertions, 2 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9edc77e39..43679113c 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -74,11 +74,12 @@ ostream& operator<<(ostream& out, const CommandStatus* s) throw() { /* class Command */ -Command::Command() throw() : d_commandStatus(NULL) { +Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { } Command::Command(const Command& cmd) { d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); + d_muted = cmd.d_muted; } Command::~Command() throw() { @@ -98,7 +99,9 @@ bool Command::fail() const throw() { void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); - printResult(out); + if(!(isMuted() && ok())) { + printResult(out); + } } std::string Command::toString() const throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 9877044fb..8e5983403 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -193,6 +193,12 @@ protected: */ const CommandStatus* d_commandStatus; + /** + * True if this command is "muted"---i.e., don't print "success" on + * successful execution. + */ + bool d_muted; + public: typedef CommandPrintSuccess printsuccess; @@ -210,6 +216,16 @@ public: std::string toString() const throw(); /** + * If false, instruct this Command not to print a success message. + */ + void setMuted(bool muted) throw() { d_muted = muted; } + + /** + * Determine whether this Command will print a success message. + */ + bool isMuted() throw() { return d_muted; } + + /** * Either the command hasn't run yet, or it completed successfully * (CommandSuccess, not CommandUnsupported or CommandFailure). */ |