fix for hiding prompt/header in shell, error-behavior options as in SMTLIB

3 files changed, 20 insertions, 14 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index adc40a9d1..c2b879a6b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -246,17 +246,19 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
 #endif /* PORTFOLIO_BUILD */
       InteractiveShell shell(*exprMgr, opts);
-      Message() << Configuration::getPackageName()
-                << " " << Configuration::getVersionString();
-      if(Configuration::isGitBuild()) {
-        Message() << " [" << Configuration::getGitId() << "]";
-      } else if(Configuration::isSubversionBuild()) {
-        Message() << " [" << Configuration::getSubversionId() << "]";
+      if(opts[options::interactivePrompt]) {
+        Message() << Configuration::getPackageName()
+                  << " " << Configuration::getVersionString();
+        if(Configuration::isGitBuild()) {
+          Message() << " [" << Configuration::getGitId() << "]";
+        } else if(Configuration::isSubversionBuild()) {
+          Message() << " [" << Configuration::getSubversionId() << "]";
+        }
+        Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+                  << " assertions:"
+                  << (Configuration::isAssertionBuild() ? "on" : "off")
+                  << endl;
       }
-      Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-                << " assertions:"
-                << (Configuration::isAssertionBuild() ? "on" : "off")
-                << endl;
       if(replayParser != NULL) {
         // have the replay parser use the declarations input interactively
         replayParser->useDeclarationsFrom(shell.getParser());
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 63a60c7a2..90229861f 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -192,7 +192,7 @@ restart:
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    if(d_options[options::verbosity] >= 0) {
+    if(d_options[options::interactivePrompt]) {
       if(line == "") {
         d_out << "CVC4> " << flush;
       } else {
@@ -260,7 +260,7 @@ restart:
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "... > " : "");
+        lineBuf = ::readline(d_options[options::interactivePrompt] ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -268,7 +268,7 @@ restart:
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        if(d_options[options::verbosity] >= 0) {
+        if(d_options[options::interactivePrompt]) {
           d_out << "... > " << flush;
         }
 
diff --git a/src/main/options b/src/main/options
index 09b06bd07..d84482836 100644
--- a/src/main/options
+++ b/src/main/options
@@ -39,9 +39,13 @@ option fallbackSequential  --fallback-sequential bool :default false
 option incrementalParallel --incremental-parallel bool :default false :link --incremental
  Use parallel solver even in incremental mode (may print 'unknown's at times)
 
-option interactivePrompt /--no-interactive-prompt bool :default true
+undocumented-option interactivePrompt /--no-interactive-prompt bool :default true
  turn off interactive prompting while in interactive mode
 
+# error behaviors
+option continuedExecution --continued-execution/--immediate-exit bool :default false :link "--interactive --no-interactive-prompt"/
+ continue executing commands, even on error
+
 option segvSpin --segv-spin bool :default false
  spin on segfault/other crash waiting for gdb
 undocumented-alias --segv-nospin = --no-segv-spin