diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8f1b1b3a1..1120bc8cd 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 e35b6f26b..0318f8ff0 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);