From d47412d2012276b97ef55ec5d95dd9d14f657888 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Sep 2014 20:39:41 -0700 Subject: [PATCH] fix(frontends/lean/parser): error line numbers for lua code, fixes #194 --- src/frontends/lean/parser.cpp | 5 +++++ src/frontends/lean/parser.h | 1 + 2 files changed, 6 insertions(+) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8f1b1b3a11..1120bc8cd7 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -205,6 +205,11 @@ void parser::display_error(exception const & ex) { ::lean::display_error(regular_stream(), &pos_provider, ex); } +void parser::display_error(script_exception const & ex) { + parser_pos_provider pos_provider(m_pos_table, get_stream_name(), m_last_script_pos); + ::lean::display_error(regular_stream(), &pos_provider, ex); +} + void parser::throw_parser_exception(char const * msg, pos_info p) { throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e35b6f26bf..0318f8ff01 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -112,6 +112,7 @@ class parser { void display_error(char const * msg, unsigned line, unsigned pos); void display_error(char const * msg, pos_info p); void display_error(exception const & ex); + void display_error(script_exception const & ex); void throw_parser_exception(char const * msg, pos_info p); void throw_nested_exception(exception & ex, pos_info p);