From 559b96ab3ed4723871a367c4408aab8ec2357fae Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 13 Oct 2016 15:12:26 -0400 Subject: [PATCH] feat(shell/server): parse file again if imports have changed --- src/shell/server.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/shell/server.cpp b/src/shell/server.cpp index d27789eae1..f4d158ffa4 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -6,6 +6,7 @@ Author: Gabriel Ebner */ #include "frontends/lean/parser.h" +#include "library/module.h" #include "shell/server.h" #include @@ -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(1, 0); + if (m_only_checked_until) { snapshot_vector new_snapshots; for (snapshot const & snap : m_snapshots) {