diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2012-12-12 17:28:14 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 15:36:53 -0400 |
commit | 04e3d0ae6b6135f50cf119f3cf85150dcc87d774 (patch) | |
tree | 9e3bf2583ccbe75fdf5a78129a9d792b7e5681a3 /src/main/interactive_shell.cpp | |
parent | 0c661d41f7594ee3c761b173c1e709ce428ce89d (diff) |
Interactive mode support for multiline input
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r-- | src/main/interactive_shell.cpp | 46 |
1 files changed, 31 insertions, 15 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index c1d2c2bb1..cba896e4e 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -162,9 +162,15 @@ InteractiveShell::~InteractiveShell() { } Command* InteractiveShell::readCommand() { + char* lineBuf = NULL; + string line = ""; + +restart: + /* Don't do anything if the input is closed or if we've seen a * QuitCommand. */ - if( d_in.eof() || d_quit ) { + if(d_in.eof() || d_quit) { + d_out << endl; return NULL; } @@ -173,30 +179,32 @@ Command* InteractiveShell::readCommand() { throw ParserException("Interactive input broken."); } - char* lineBuf = NULL; - string input; - stringbuf sb; - string line; - /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : ""); + lineBuf = ::readline(d_options[options::verbosity] >= 0 ? (line == "" ? "CVC4> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } - line = lineBuf == NULL ? "" : lineBuf; + line += lineBuf == NULL ? "" : lineBuf; free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { if(d_options[options::verbosity] >= 0) { - d_out << "CVC4> " << flush; + if(line == "") { + d_out << "CVC4> " << flush; + } else { + d_out << "... > " << flush; + } } /* Read a line */ - d_in.get(sb,'\n'); - line = sb.str(); + stringbuf sb; + d_in.get(sb); + line += sb.str(); } + + string input = ""; while(true) { Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; @@ -221,20 +229,24 @@ Command* InteractiveShell::readCommand() { (d_usingReadline && lineBuf == NULL) ) { input += line; - if( input.empty() ) { + if(input.empty()) { /* Nothing left to parse. */ + d_out << endl; return NULL; } /* Some input left to parse, but nothing left to read. Jump out of input loop. */ - break; + d_out << endl; + input = line = ""; + d_in.clear(); + goto restart; } if(!d_usingReadline) { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - assert( c == '\n' ); + assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } @@ -259,7 +271,8 @@ Command* InteractiveShell::readCommand() { } /* Read a line */ - d_in.get(sb,'\n'); + stringbuf sb; + d_in.get(sb); line = sb.str(); } } else { @@ -296,6 +309,9 @@ Command* InteractiveShell::readCommand() { #endif /* HAVE_LIBREADLINE */ } } + } catch(ParserEndOfFileException& pe) { + line += "\n"; + goto restart; } catch(ParserException& pe) { d_out << pe << endl; // We can't really clear out the sequence and abort the current line, |