From 3136f36ed6f7fc8079fe43855fb8b54bd3a46cc5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 3 Jan 2017 18:38:51 +0100 Subject: [PATCH] fix(frontends/lean/parser): complete after periods trailing identifiers --- src/frontends/lean/parser.cpp | 19 +++++++++++++++---- tests/lean/interactive/complete.input | 2 ++ .../interactive/complete.input.expected.out | 2 ++ .../complete_trailing_period.input | 2 ++ ...omplete_trailing_period.input.expected.out | 2 ++ 5 files changed, 23 insertions(+), 4 deletions(-) create mode 100644 tests/lean/interactive/complete.input create mode 100644 tests/lean/interactive/complete.input.expected.out create mode 100644 tests/lean/interactive/complete_trailing_period.input create mode 100644 tests/lean/interactive/complete_trailing_period.input.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 5afa1f811d..633bfc828e 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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) { diff --git a/tests/lean/interactive/complete.input b/tests/lean/interactive/complete.input new file mode 100644 index 0000000000..473d4c1ee6 --- /dev/null +++ b/tests/lean/interactive/complete.input @@ -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} diff --git a/tests/lean/interactive/complete.input.expected.out b/tests/lean/interactive/complete.input.expected.out new file mode 100644 index 0000000000..b843f016bd --- /dev/null +++ b/tests/lean/interactive/complete.input.expected.out @@ -0,0 +1,2 @@ +{"message":"file invalidated","response":"ok","seq_num":0} +{"prefix":"tt","response":"ok","seq_num":1} diff --git a/tests/lean/interactive/complete_trailing_period.input b/tests/lean/interactive/complete_trailing_period.input new file mode 100644 index 0000000000..6a6a5a60a7 --- /dev/null +++ b/tests/lean/interactive/complete_trailing_period.input @@ -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} diff --git a/tests/lean/interactive/complete_trailing_period.input.expected.out b/tests/lean/interactive/complete_trailing_period.input.expected.out new file mode 100644 index 0000000000..d0a2e3b9e8 --- /dev/null +++ b/tests/lean/interactive/complete_trailing_period.input.expected.out @@ -0,0 +1,2 @@ +{"message":"file invalidated","response":"ok","seq_num":0} +{"prefix":"bool.","response":"ok","seq_num":1}