feat(emacs): implement show-goal-at-pos using faster info manager

src/emacs/lean-mode.el

@@ -52,19 +52,6 @@
               (or arg "")
               (shell-quote-argument (f-full target-file-name))))))
 
-(defun lean-show-goal-at-pos ()
-  "Show goal at the current point."
-  (interactive)
-  (lean-server-sync)
-  (lean-server-send-command
-   (list :command "show_goal"
-         :line (line-number-at-pos)
-         :col (current-column))
-   (cl-function
-    (lambda (&key state) (with-output-to-lean-info (princ state))))
-   (cl-function
-    (lambda (&key message) (with-output-to-lean-info (princ message))))))
-
 (defun lean-std-exe ()
   (interactive)
   (lean-execute))

src/emacs/lean-settings.el

@@ -122,11 +122,6 @@ false (nil)."
   :group 'lean
   :type 'boolean)
 
-(defcustom lean-show-proofstate-in-minibuffer nil
-  "Set this variable to true to show proof state at minibuffer."
-  :group 'lean
-  :type 'boolean)
-
 (defcustom lean-proofstate-display-style 'show-first-and-other-conclusions
   "Choose how to display proof state in *lean-info* buffer."
   :group 'lean

src/emacs/lean-type.el

@@ -85,20 +85,12 @@
 
 (defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
   "Continuation for lean-eldoc-documentation-function"
-  (let* ((info-string (lean-info-record-to-string info-record))
-         (proofstate (plist-get info-record :proofstate)))
+  (let ((info-string (lean-info-record-to-string info-record)))
     (when info-string
       (when add-to-kill-ring
         (kill-new
          (substring-no-properties info-string)))
-      ;; Display on Mini-buffer
-      (when (or lean-show-proofstate-in-minibuffer
-                (not proofstate))
-        (message "%s" info-string))
-      ;; Display on Info Buffer
-      ; (with-output-to-lean-info
-                                        ; (princ info-string))
-      )))
+      (message "%s" info-string))))
 
 (defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
   "Show information of lean expression at point if any"
@@ -113,4 +105,13 @@
   (interactive)
   (lean-eldoc-documentation-function lean-show-type-add-to-kill-ring))
 
+(defun lean-show-goal-at-pos ()
+  "Show goal at the current point."
+  (interactive)
+  (lean-get-info-record-at-point
+   (lambda (info-record)
+     (-if-let (state (plist-get info-record :state))
+         (with-output-to-lean-info (princ state))
+       (message "No goal found at point")))))
+
 (provide 'lean-type)

src/frontends/lean/elaborator.cpp

@@ -110,10 +110,6 @@ elaborator::elaborator(environment const & env, options const & opts, metavar_co
                        local_context const & lctx, optional<info_manager> & infom):
     m_env(env), m_opts(opts),
     m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_owns_infom(infom) {
-    unsigned line, col;
-    if (has_show_goal(m_opts, line, col)) {
-        m_show_goal_pos = pos_info(line, col);
-    }
     if (infom) {
         g_infom = &*infom;
     }
@@ -2348,26 +2344,6 @@ tactic_state elaborator::mk_tactic_state_for(expr const & mvar) {
     return ::lean::mk_tactic_state_for(m_env, m_opts, mctx, lctx, type);
 }
 
-void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr const & end_ref, expr const & curr_ref) {
-    if (!m_show_goal_pos) return;
-    pos_info_provider * provider = get_pos_info_provider();
-    if (!provider) return;
-    unsigned line  = m_show_goal_pos->first;
-    unsigned col   = m_show_goal_pos->second;
-    auto start_pos = provider->get_pos_info(start_ref);
-    auto end_pos   = provider->get_pos_info(end_ref);
-    auto curr_pos  = provider->get_pos_info(curr_ref);
-    if (!start_pos || !end_pos || !curr_pos)
-        return;
-    if (start_pos->first > line || (start_pos->first == line && start_pos->second > col))
-        return;
-    if (end_pos->first < line || (end_pos->first == line && end_pos->second < col))
-        return;
-    if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col))
-        return;
-    throw show_goal_exception(*curr_pos, s);
-}
-
 /* Apply the given tactic to the state 's'.
    Report any errors detected during the process using position information associated with 'ref'. */
 tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
@@ -2411,8 +2387,6 @@ tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const
 
 tactic_state elaborator::execute_begin_end_tactics(buffer<expr> const & tactics, tactic_state const & s, expr const & ref) {
     lean_assert(!tactics.empty());
-    expr start_ref = tactics[0];
-    expr end_ref   = ref;
     list<expr> gs = s.goals();
     if (!gs) throw elaborator_exception(ref, "tactic failed, there are no goals to be solved");
     tactic_state new_s = set_goals(s, to_list(head(gs)));
@@ -2420,7 +2394,6 @@ tactic_state elaborator::execute_begin_end_tactics(buffer<expr> const & tactics,
         expr const & curr_ref = tactic;
         trace_elab_debug(tout() << "executing tactic:\n" << tactic << "\n";);
         if (is_begin_end_element(tactic)) {
-            show_goal(new_s, start_ref, end_ref, curr_ref);
             add_tactic_state_info(new_s, curr_ref);
             new_s = execute_tactic(get_annotation_arg(tactic), new_s, curr_ref);
         } else if (is_begin_end_block(tactic)) {
@@ -2431,8 +2404,7 @@ tactic_state elaborator::execute_begin_end_tactics(buffer<expr> const & tactics,
             throw elaborator_exception(curr_ref, "ill-formed 'begin ... end' tactic block");
         }
     }
-    add_tactic_state_info(new_s, end_ref);
-    show_goal(new_s, start_ref, end_ref, end_ref);
+    add_tactic_state_info(new_s, ref);
     if (new_s.goals()) throw_unsolved_tactic_state(new_s, "tactic failed, there are unsolved goals", ref);
     return set_goals(new_s, tail(gs));
 }
@@ -2460,7 +2432,6 @@ void elaborator::invoke_begin_end_tactics(expr const & mvar, buffer<expr> const
 void elaborator::invoke_atomic_tactic(expr const & mvar, expr const & tactic) {
     expr const & ref = mvar;
     tactic_state s       = mk_tactic_state_for(mvar);
-    show_goal(s, tactic, mvar, tactic);
     add_tactic_state_info(s, ref);
     trace_elab(tout() << "initial tactic state\n" << s.pp() << "\n";);
     tactic_state new_s   = execute_tactic(tactic, s, ref);
@@ -2579,12 +2550,6 @@ void elaborator::ensure_no_unassigned_metavars(expr const & e) {
             if (!has_expr_metavar(e)) return false;
             if (is_metavar_decl_ref(e) && !mctx.is_assigned(e)) {
                 tactic_state s = mk_tactic_state_for(e);
-                if (m_show_goal_pos && get_pos_info_provider()) {
-                    if (auto pos = get_pos_info_provider()->get_pos_info(e)) {
-                        if (pos == m_show_goal_pos)
-                            throw show_goal_exception(*pos, s);
-                    }
-                }
                 throw_unsolved_tactic_state(s, "don't know how to synthesize placeholder", e);
             }
             return true;

src/frontends/lean/elaborator.h

@@ -89,9 +89,6 @@ private:
 
     bool              m_in_pattern{false};
 
-    /* Position information for show goal feature */
-    optional<pos_info> m_show_goal_pos;
-
     expr get_default_numeral_type();
 
     typedef std::function<format(expr const &)> pp_fn;
@@ -220,7 +217,6 @@ private:
     expr visit(expr const & e, optional<expr> const & expected_type);
 
     void add_tactic_state_info(tactic_state const & s, expr const & ref);
-    void show_goal(tactic_state const & s, expr const & start_ref, expr const & end_ref, expr const & curr_ref);
     tactic_state mk_tactic_state_for(expr const & mvar);
     tactic_state execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
     tactic_state execute_begin_end_tactics(buffer<expr> const & tactics, tactic_state const & s, expr const & ref);

src/shell/server.cpp

@@ -88,8 +88,6 @@ json server::handle_request(json const & req) {
         return handle_check(req);
     } else if (command == "complete") {
         return handle_complete(req);
-    } else if (command == "show_goal") {
-        return handle_show_goal(req);
     } else if (command == "info") {
         return handle_info(req);
     }
@@ -348,44 +346,6 @@ json server::handle_complete(json const & req) {
     return res;
 }
 
-json server::handle_show_goal(json const &req) {
-    pos_info pos(req["line"], req["col"]);
-
-    if (!m_snapshots.size()) handle_check({});
-
-    snapshot * snap = nullptr;
-    for (auto & s : m_snapshots) {
-        if (s.m_pos.first < pos.first)
-            snap = &s;
-    }
-
-    std::istringstream in(m_content);
-    bool use_exceptions = false;
-    optional<std::string> base_dir;
-    parser p(m_initial_env, m_ios, in, m_file_name.c_str(),
-             base_dir, use_exceptions, m_num_threads, snap);
-
-    p.enable_show_goal(pos);
-
-    try {
-        p();
-    } catch (show_goal_exception & ex) {
-        json res;
-        res["response"] = "ok";
-        res["line"] = ex.m_pos.first;
-        res["col"] = ex.m_pos.second;
-        std::stringstream buf;
-        buf << ex.m_state.pp();
-        res["state"] = buf.str();
-        return res;
-    }
-
-    json res;
-    res["response"] = "error";
-    res["message"] = "could not find goal";
-    return res;
-}
-
 json server::handle_info(json const & req) {
     unsigned line = req["line"];
     unsigned col = req["column"];

src/shell/server.h

@@ -34,7 +34,6 @@ class server {
     json handle_sync(json const & req);
     json handle_check(json const & req);
     json handle_complete(json const & req);
-    json handle_show_goal(json const & req);
     json handle_info(json const & req);
 
     json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o);