From 2a37611d1f5ff9e88c19c9832f12363861ab8eca Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 10 Nov 2016 20:31:07 +0100 Subject: [PATCH] feat(emacs): implement show-goal-at-pos using faster info manager --- src/emacs/lean-mode.el | 13 ---------- src/emacs/lean-settings.el | 5 ---- src/emacs/lean-type.el | 21 ++++++++-------- src/frontends/lean/elaborator.cpp | 37 +--------------------------- src/frontends/lean/elaborator.h | 4 ---- src/shell/server.cpp | 40 ------------------------------- src/shell/server.h | 1 - 7 files changed, 12 insertions(+), 109 deletions(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 276595d794..62a57c3423 100644 --- a/src/emacs/lean-mode.el +++ b/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)) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index fee099eb14..67c1e78eba 100644 --- a/src/emacs/lean-settings.el +++ b/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 diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 424c3217c7..ff4598b4e8 100644 --- a/src/emacs/lean-type.el +++ b/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) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0ed18ce48e..cbc9c5c562 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -110,10 +110,6 @@ elaborator::elaborator(environment const & env, options const & opts, metavar_co local_context const & lctx, optional & 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 const & tactics, tactic_state const & s, expr const & ref) { lean_assert(!tactics.empty()); - expr start_ref = tactics[0]; - expr end_ref = ref; list 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 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 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 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; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 17b858034c..066396d434 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -89,9 +89,6 @@ private: bool m_in_pattern{false}; - /* Position information for show goal feature */ - optional m_show_goal_pos; - expr get_default_numeral_type(); typedef std::function pp_fn; @@ -220,7 +217,6 @@ private: expr visit(expr const & e, optional 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 const & tactics, tactic_state const & s, expr const & ref); diff --git a/src/shell/server.cpp b/src/shell/server.cpp index d3cb3db336..ea298adfee 100644 --- a/src/shell/server.cpp +++ b/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 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"]; diff --git a/src/shell/server.h b/src/shell/server.h index 4b582483f9..226a727969 100644 --- a/src/shell/server.h +++ b/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);