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

fix(shell/server): let completion fall back to first (imports) snapshot

Browse source
This commit is contained in:
Sebastian Ullrich 2016-10-16 19:08:44 -04:00 • committed by Leonardo de Moura
parent 7f4cbdf402
commit ce28e1aedb
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/shell/server.cpp
View file

@ -176,7 +176,7 @@ json server::handle_check(json const &) {
}
snapshot const * server::get_closest_snapshot(unsigned line) {
snapshot const * ret = nullptr;
snapshot const * ret = m_snapshots.size() ? &m_snapshots.front() : nullptr;
for (snapshot const & snap : m_snapshots) {
if (snap.m_pos.first <= line)
ret = &snap;
@ -274,6 +274,10 @@ json server::handle_complete(json const & req) {
unsigned line = req["line"];
std::vector<json> completions;
if (!m_snapshots.size()) { // should only happen when imports have been touched
handle_check({});
}
if (snapshot const * snap = get_closest_snapshot(line)) {
environment const & env = snap->m_env;
options const & opts = snap->m_options;