diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:44 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:44 +0000 |
commit | dfa8ba577b55318919caae4cd3d03c26eee39944 (patch) | |
tree | 89beafa1e4cb2be12a86dd3994c9926e6955f3ab /src/main | |
parent | 3870dd8a11c1153e2db24ffe1b384b84129c2df4 (diff) |
Saving state between lines in interactive mode (Fixes: #223)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/interactive_shell.cpp | 5 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 6 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 7af72ed2d..3d37ade43 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -93,6 +93,7 @@ Command* InteractiveShell::readCommand() { Parser *parser = d_parserBuilder .withStringInput(input) + .withStateFrom(d_lastParser) .build(); /* There may be more than one command in the input. Build up a @@ -104,7 +105,9 @@ Command* InteractiveShell::readCommand() { cmd_seq->addCommand(cmd); } - delete parser; + delete d_lastParser; + d_lastParser = parser; + return cmd_seq; } diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 66c134ecd..8f207145e 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -29,17 +29,19 @@ namespace CVC4 { using namespace parser; -class InteractiveShell { +class CVC4_PUBLIC InteractiveShell { std::istream& d_in; std::ostream& d_out; ParserBuilder d_parserBuilder; + Parser* d_lastParser; public: InteractiveShell(ParserBuilder& parserBuilder, const Options& options) : d_in(*options.in), d_out(*options.out), - d_parserBuilder(parserBuilder) { + d_parserBuilder(parserBuilder), + d_lastParser(NULL) { } /** Read a command from the interactive shell. This will read as |