fix(frontends/lean/interactive): fix info on new field notation

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<info_manager> const & info_managers, break_at_pos_exception const & e, json & j) {
+                 std::vector<info_manager> 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<vm_obj_format_info const *>(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);
         }

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<info_manager> const & info_managers, break_at_pos_exception const & e, json & j);
+                 std::vector<info_manager> const & info_managers, pos_info const & pos,
+                 break_at_pos_exception const & e, json & j);
 
 void initialize_interactive();
 void finalize_interactive();

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();

src/shell/server.cpp

@@ -579,7 +579,7 @@ json server::info(std::shared_ptr<module_info const> 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;

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