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

fix(frontends/lean/interactive): fix empty prefix in autocompletion

Browse source
This commit is contained in:
Gabriel Ebner 2017-08-01 18:42:31 +01:00
parent 6d0a7a80af
commit 403234f29e
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/interactive.cpp
View file

@ -60,7 +60,8 @@ void report_completions(environment const & env, options const & opts, pos_info
search_path const & path, char const * mod_path, break_at_pos_exception const & e, json & j) {
g_context = e.m_token_info.m_context;
unsigned offset = pos.second - e.m_token_info.m_pos.second;
std::string prefix = e.m_token_info.m_token.to_string();
// TODO(gabriel): this is broken with french quotes
std::string prefix = e.m_token_info.m_token == name("") ? "" : e.m_token_info.m_token.to_string();
if (auto stop = utf8_char_pos(prefix.c_str(), offset))
prefix = prefix.substr(0, *stop);
switch (e.m_token_info.m_context) {