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

chore(frontends/lean/parser): style

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-20 18:38:58 -08:00
parent bbc99d4aa5
commit c62014df7a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/parser.cpp
View file

@ -201,9 +201,9 @@ void parser::check_break_at_pos(break_at_pos_exception::token_context ctxt) {
auto p = pos();
if (m_break_at_pos && p.first == m_break_at_pos->first && p.second <= m_break_at_pos->second) {
name tk;
if (curr_is_identifier())
if (curr_is_identifier()) {
tk = get_name_val();
else if (curr_is_command() || curr_is_keyword()) {
} else if (curr_is_command() || curr_is_keyword()) {
tk = get_token_info().token();
// When completing at the end of a token that cannot be extended into an identifier,
// start an empty completion instead (in the next call to `check_break_before/at_pos`, using the correct