diff options
Diffstat (limited to 'src/main/interactive_shell.h')
| -rw-r--r-- | src/main/interactive_shell.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index f6852b95b..65fea8494 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -40,12 +40,20 @@ class CVC4_PUBLIC InteractiveShell { bool d_quit; bool d_usingReadline; + std::string d_historyFilename; + static const std::string INPUT_FILENAME; + static const unsigned s_historyLimit = 500; public: InteractiveShell(ExprManager& exprManager, const Options& options); /** + * Close out the interactive session. + */ + ~InteractiveShell(); + + /** * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. */ |