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

feat(frontends/lean/parser): propagate position information to expressions created by macro implemented in Lua

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-20 01:07:27 -08:00
parent 3eb4de6760
commit c730dd7872
1 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -848,6 +848,17 @@ class parser::imp {
} }
} }
void propagage_position(expr const & e, pos_info p) {
for_each(e, [&](expr const & e, unsigned) {
if (m_expr_pos_info.find(e) == m_expr_pos_info.end()) {
save(e, p);
return true;
} else {
return false; // do not search children...
}
});
}
bool is_curr_begin_expr() const { bool is_curr_begin_expr() const {
switch (curr()) { switch (curr()) {
case scanner::token::RightParen: case scanner::token::RightParen:
@ -955,7 +966,8 @@ class parser::imp {
if (is_expr(L, -1)) { if (is_expr(L, -1)) {
expr r = to_expr(L, -1); expr r = to_expr(L, -1);
lua_pop(L, 1); lua_pop(L, 1);
return save(r, p); propagage_position(r, p);
return r;
} else { } else {
lua_pop(L, 1); lua_pop(L, 1);
throw parser_error("failed to execute macro", p); throw parser_error("failed to execute macro", p);
@ -971,7 +983,7 @@ class parser::imp {
luaref proc = m.second; luaref proc = m.second;
macro_arg_stack args; macro_arg_stack args;
return parse_macro(arg_kinds, proc, args, p); return parse_macro(arg_kinds, proc, args, p);
} }
/** /**
\brief Parse an identifier that has a "null denotation" (See \brief Parse an identifier that has a "null denotation" (See