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

fix(frontends/lean/parser): complete after periods trailing identifiers

Browse source
This commit is contained in:
Sebastian Ullrich 2017-01-03 18:38:51 +01:00 • committed by Leonardo de Moura
parent 7770e87f69
commit 3136f36ed6
5 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -208,11 +208,22 @@ bool parser::check_break_at_pos(pos_info const & p, name const & tk) {
}
void parser::scan() {
if (curr_is_identifier() && check_break_at_pos(pos(), get_name_val()))
throw break_at_pos_exception(pos(), get_name_val(), break_at_pos_exception::token_context::ident);
if (m_break_at_pos && *m_break_at_pos < pos())
if (m_break_at_pos && curr_is_identifier()) {
pos_info curr_pos = pos();
name curr_ident = get_name_val();
if (check_break_at_pos(curr_pos, curr_ident))
throw break_at_pos_exception(curr_pos, curr_ident, break_at_pos_exception::token_context::ident);
m_curr = m_scanner.scan(m_env);
// when breaking on a '.' token trailing an identifier, report them as a single, concatenated token
if (m_break_at_pos->first == curr_pos.first &&
m_break_at_pos->second == curr_pos.second + curr_ident.utf8_size() && curr_is_token(get_period_tk()))
throw break_at_pos_exception(curr_pos, name(curr_ident.to_string() + get_period_tk()),
break_at_pos_exception::token_context::ident);
} else if (m_break_at_pos && *m_break_at_pos < pos()) {
throw break_at_pos_exception();
m_curr = m_scanner.scan(m_env);
} else {
m_curr = m_scanner.scan(m_env);
}
}
expr parser::mk_sorry(pos_info const & p) {

2
tests/lean/interactive/complete.input Normal file
View file

@ -0,0 +1,2 @@
{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := tt"}
{"seq_num": 1, "command": "complete", "file_name": "f", "line": 1, "column": 11, "skip_completions": true}

2
tests/lean/interactive/complete.input.expected.out Normal file
View file

@ -0,0 +1,2 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"prefix":"tt","response":"ok","seq_num":1}

2
tests/lean/interactive/complete_trailing_period.input Normal file
View file

@ -0,0 +1,2 @@
{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := bool."}
{"seq_num": 1, "command": "complete", "file_name": "f", "line": 1, "column": 14, "skip_completions": true}

2
tests/lean/interactive/complete_trailing_period.input.expected.out Normal file
View file

@ -0,0 +1,2 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"prefix":"bool.","response":"ok","seq_num":1}