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

fix(frontends/lean/info_manager): crash when accessing INFO in the end of the file

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-29 16:39:43 -07:00
parent a0c37b231f
commit 334977b8bd
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/info_manager.cpp
View file

@ -597,7 +597,9 @@ struct info_manager::imp {
lean_assert(it != m_env_info.end() && it->m_line <= linenum); lean_assert(it != m_env_info.end() && it->m_line <= linenum);
auto next = it; auto next = it;
next++; next++;
if (next == m_env_info.end() || next->m_line > linenum) if (next == m_env_info.end())
return optional<pair<environment, options>>(mk_pair(it->m_env, it->m_options));
if (next->m_line > linenum)
return optional<pair<environment, options>>(mk_pair(next->m_env, next->m_options)); return optional<pair<environment, options>>(mk_pair(next->m_env, next->m_options));
it = next; it = next;
} }