diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 6ce628698..f14909853 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -442,9 +442,7 @@ struct info_manager::imp { void display(environment const & env, io_state const & ios, unsigned line) { lock_guard 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); diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index e642cbef4..a15ad64a5 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -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; }