From 3c8e176fb098cb61b3ebb91e2418efcc4e76cfe1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 30 Mar 2017 14:17:36 +0200 Subject: [PATCH] fix(frontends/lean/interactive): fix info on new field notation --- src/frontends/lean/interactive.cpp | 13 ++++++++++++- src/frontends/lean/interactive.h | 3 ++- src/frontends/lean/parser.cpp | 2 +- src/shell/server.cpp | 2 +- tests/lean/interactive/field_info.lean | 10 +++++----- 5 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 7efd6aff4d..5fa9ffbd7f 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -93,7 +93,8 @@ void report_completions(environment const & env, options const & opts, pos_info } void report_info(environment const & env, options const & opts, io_state const & ios, module_info const & m_mod_info, - std::vector const & info_managers, break_at_pos_exception const & e, json & j) { + std::vector const & info_managers, pos_info const & pos, + break_at_pos_exception const & e, json & j) { g_context = e.m_token_info.m_context; json record; @@ -148,6 +149,16 @@ void report_info(environment const & env, options const & opts, io_state const & return dynamic_cast(d.raw()); }); } + // first check for field infos inside token + for (name pre = tk.get_prefix(); !has_token_info && pre; pre = pre.get_prefix()) { + auto field_pos = e.m_token_info.m_pos; + field_pos.second += pre.utf8_size(); + if (pos.second >= field_pos.second && + infom.get_line_info_set(field_pos.first).find(field_pos.second)) { + infom.get_info_record(env, opts, ios, field_pos, record); + has_token_info = true; + } + } if (!has_token_info) infom.get_info_record(env, opts, ios, e.m_token_info.m_pos, record); } diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h index c8ab7b491e..b5b091a25c 100644 --- a/src/frontends/lean/interactive.h +++ b/src/frontends/lean/interactive.h @@ -14,7 +14,8 @@ void interactive_report_type(environment const & env, options const & opts, expr void report_completions(environment const & env, options const & opts, pos_info const & pos, bool skip_completions, char const * mod_path, break_at_pos_exception const & e, json & j); void report_info(environment const & env, options const & opts, io_state const & ios, module_info const & m_mod_info, - std::vector const & info_managers, break_at_pos_exception const & e, json & j); + std::vector const & info_managers, pos_info const & pos, + break_at_pos_exception const & e, json & j); void initialize_interactive(); void finalize_interactive(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0462e50f10..eb9ba33234 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -181,7 +181,7 @@ 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() || curr() == token_kind::FieldName) { tk = get_name_val(); } else if (curr_is_command() || curr_is_keyword()) { tk = get_token_info().token(); diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 4fa1d9bf47..d9d84dc6db 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -579,7 +579,7 @@ json server::info(std::shared_ptr const & mod_info, pos_info env = snap->m_snapshot_at_end->m_env; opts = snap->m_snapshot_at_end->m_options; } - report_info(env, opts, m_ios, *mod_info, get_info_managers(m_lt), e, j); + report_info(env, opts, m_ios, *mod_info, get_info_managers(m_lt), pos, e, j); } catch (throwable & ex) {} return j; diff --git a/tests/lean/interactive/field_info.lean b/tests/lean/interactive/field_info.lean index 831005b55d..f4f9a7b1e0 100644 --- a/tests/lean/interactive/field_info.lean +++ b/tests/lean/interactive/field_info.lean @@ -1,12 +1,12 @@ -def f (n : ℕ) := n^.to_string - --^ "command": "info" -def g (l : list ℕ) := l^.all +def f (n : ℕ) := n.to_string + --^ "command": "info" +def g (l : list ℕ) := l.all --^ "command": "info" -- elaborated, not locally inferable def h : list ℕ → (ℕ → bool) → bool := -λ l, (l ++ l)^.all - --^ "command": "info" +λ l, (l ++ l).all + --^ "command": "info" -- not elaborated, locally inferable def j := (list.nil^.all