max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(shell/server): parse file again if imports have changed

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-13 15:12:26 -04:00 • committed by Leonardo de Moura
parent b14a0c43ff
commit 559b96ab3e
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/shell/server.cpp
View file

@ -6,6 +6,7 @@ Author: Gabriel Ebner
*/
#include "frontends/lean/parser.h"
#include "library/module.h"
#include "shell/server.h"
#include <list>
@ -107,6 +108,9 @@ json server::handle_sync(json const & req) {
}
json server::handle_check(json const &) {
if (imports_have_changed(m_checked_env))
m_only_checked_until = optional<pos_info>(1, 0);
if (m_only_checked_until) {
snapshot_vector new_snapshots;
for (snapshot const & snap : m_snapshots) {