michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): display elaborator error messages

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 18:48:53 -07:00
parent ca6a6d71e5
commit df07a84d11
1 changed files with 17 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/frontends/lean/parser.cpp
View file

@ -1522,13 +1522,23 @@ class parser::imp {
sync();
}
void display_error(elaborator_exception const &) {
#if 0
// TODO(Leo)
display_error_pos(m_elaborator.get_original(ex.get_expr()));
regular(m_frontend) << " " << ex << endl;
sync();
#endif
struct lean_pos_info_provider : public pos_info_provider {
imp const & m_ref;
lean_pos_info_provider(imp const & r):m_ref(r) {}
virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const {
expr const & o = m_ref.m_elaborator.get_original(e);
auto it = m_ref.m_expr_pos_info.find(o);
if (it == m_ref.m_expr_pos_info.end())
throw exception("position is not available"); // information is not available
return it->second;
}
};
void display_error(elaborator_exception const & ex) {
formatter fmt = m_frontend.get_state().get_formatter();
options opts = m_frontend.get_state().get_options();
lean_pos_info_provider pos_provider(*this);
regular(m_frontend) << ex.get_justification().pp(fmt, opts, &pos_provider, true) << endl;
}
void updt_options() {