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

fix(frontends/lean/parser): caching problem when using "show hole" and "show goal" command line options

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-27 18:55:20 -07:00
parent 0786841c71
commit d50fa26ca2
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -190,11 +190,16 @@ void parser::add_abbrev_index(name const & a, name const & d) {
}
bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
if (!m_info_manager)
return true; // we are not tracking info
for (unsigned i = start_line; i <= end_line; i++)
if (m_info_manager->is_invalidated(i))
if (m_stop_at) {
if (start_line <= m_stop_at_line && m_stop_at_line <= end_line)
return false;
}
if (m_info_manager) {
// we are tracking info
for (unsigned i = start_line; i <= end_line; i++)
if (m_info_manager->is_invalidated(i))
return false;
}
return true;
}