Forcing a type check on Node construction in debug mode (Fixes: #188)

NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

1 files changed, 10 insertions, 0 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2bad12e2c..f73e268a3 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -234,6 +234,11 @@ Command* Parser::nextCommand() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -252,6 +257,11 @@ Expr Parser::nextExpression() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextExpression() => " << result << std::endl;