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/parser | |
parent | 0c661d41f7594ee3c761b173c1e709ce428ce89d (diff) |
Interactive mode support for multiline input
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.cpp | 14 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 2 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 3 | ||||
-rw-r--r-- | src/parser/input.h | 2 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 24 |
6 files changed, 38 insertions, 9 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index fbf2b8650..2279865ae 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -283,16 +283,22 @@ void AntlrInput::warning(const std::string& message) { Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; } -void AntlrInput::parseError(const std::string& message) +void AntlrInput::parseError(const std::string& message, bool eofException) throw (ParserException) { Debug("parser") << "Throwing exception: " << getInputStream()->getName() << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; - throw ParserException(message, getInputStream()->getName(), - d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); + if(eofException) { + throw ParserEndOfFileException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } else { + throw ParserException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index a2fe99f52..020db0d50 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -209,7 +209,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - void parseError(const std::string& msg) + void parseError(const std::string& msg, bool eofException = false) throw (ParserException); /** Set the ANTLR3 lexer for this input. */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 9c92846bb..07283f1af 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -261,7 +261,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } // Call the error display routine - input->parseError(ss.str()); + input->parseError(ss.str(), ((pANTLR3_COMMON_TOKEN)ex->token)->type == ANTLR3_TOKEN_EOF); } /// diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b8ec160e8..e5e26c9a2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -625,8 +625,7 @@ mainCommand[CVC4::Command*& cmd] : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] { cmd = new QueryCommand(f); } - | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK { cmd = new CheckSatCommand(); } + | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); } /* options */ | OPTION_TOK diff --git a/src/parser/input.h b/src/parser/input.h index f4b36469b..5fd3611be 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -178,7 +178,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - virtual void parseError(const std::string& msg) + virtual void parseError(const std::string& msg, bool eofException = false) throw (ParserException) = 0; /** Parse an expression from the input by invoking the diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 8abc04c15..6eae3047d 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -89,6 +89,30 @@ protected: unsigned long d_column; };/* class ParserException */ +class CVC4_PUBLIC ParserEndOfFileException : public ParserException { +public: + + // Constructors same as ParserException's + + ParserEndOfFileException() throw() : + ParserException() { + } + + ParserEndOfFileException(const std::string& msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const char* msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const std::string& msg, const std::string& filename, + unsigned long line, unsigned long column) throw() : + ParserException(msg, filename, line, column) { + } + +};/* class ParserEndOfFileException */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |