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

fix(frontends/lean/server): crash when INFO is invoked before VISIT/LOAD

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-13 18:31:47 -07:00
parent d30854829d
commit 75be034d3d
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/server.cpp
View file

@ -150,6 +150,7 @@ void server::visit_file(std::string const & fname) {
} }
void server::show_info(unsigned linenum) { void server::show_info(unsigned linenum) {
check_file();
update(); update();
unsigned i = m_file->find(linenum); unsigned i = m_file->find(linenum);
environment const & env = i == 0 ? m_env : m_file->m_snapshots[i-1].m_env; environment const & env = i == 0 ? m_env : m_file->m_snapshots[i-1].m_env;