From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 4 Apr 2014 18:49:17 +0000 (-0400)
Subject: Allow turning off the interactive prompt while in interactive mode.
X-Git-Tag: cvc5-1.0.0~6984
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=00d068f91c675edbe63c2f8c1dae283f300dd4cc;p=cvc5.git

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 a8099ca30..63a60c7a2 100644
--- 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 35e3df7d2..09b06bd07 100644
--- 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