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

feat(frontends/lean/server): add NAY and STALE status to --BEGININFO

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-02 19:04:01 -07:00
parent 974a0a4217
commit 36674eb8d9
2 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -442,9 +442,7 @@ struct info_manager::imp {
void display(environment const & env, io_state const & ios, unsigned line) {
lock_guard<mutex> lc(m_mutex);
if (line >= m_processed_upto && line < m_line_valid.size() && !m_line_valid[line]) {
regular(env, ios) << "-- NAY\n";
} else if (line >= m_line_data.size() || m_line_data[line].empty()) {
if (line >= m_line_data.size() || m_line_data[line].empty()) {
// do nothing
} else if (m_env_info.empty()) {
display_core(env, ios.get_options(), ios, line);

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

@ -361,7 +361,12 @@ void server::set_option(std::string const & line) {
void server::show_info(unsigned linenum) {
check_file();
m_out << "-- BEGININFO" << std::endl;
m_out << "-- BEGININFO";
if (m_file->infom().is_invalidated(linenum))
m_out << " STALE";
if (linenum >= m_file->infom().get_processed_upto())
m_out << " NAY";
m_out << std::endl;
m_file->infom().display(m_env, m_ios, linenum);
m_out << "-- ENDINFO" << std::endl;
}