Allow turning off the interactive prompt while in interactive mode.

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index a8099ca30d78229b8067d3ee753f3bdf250f9fa7..63a60c7a2d1ca012d45f42feeb68572b8f5f71be 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -32,6 +32,7 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "options/options.h"
+#include "main/options.h"
 #include "util/language.h"
 #include "util/output.h"
 
@@ -183,7 +184,7 @@ restart:
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline(d_options[options::verbosity] >= 0 ? (line == "" ? "CVC4> " : "... > ") : "");
+    lineBuf = ::readline(d_options[options::interactivePrompt] ? (line == "" ? "CVC4> " : "... > ") : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }

diff --git a/src/main/options b/src/main/options
index 35e3df7d293e465cc160209def0086385a470516..09b06bd07bbd281d81fc71b1b402ec74fd0270e7 100644 (file)
--- a/src/main/options
+++ b/src/main/options
@@ -39,6 +39,9 @@ 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
+ turn off interactive prompting while in interactive mode
+
 option segvSpin --segv-spin bool :default false
  spin on segfault/other crash waiting for gdb
 undocumented-alias --segv-nospin = --no-segv-spin