From bb75e6398a88f6f7dbff2e3de5f7e2e30b4f4674 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 7 Nov 2016 14:10:34 +0100 Subject: [PATCH] feat(emacs, frontends/lean/info_manager): implement 'go to definition' --- src/emacs/lean-company.el | 14 ++++++------ src/emacs/lean-info.el | 33 +++++++++++++++++++++++------ src/emacs/lean-mode.el | 2 ++ src/emacs/lean-settings.el | 3 +++ src/emacs/lean-type.el | 14 +++++------- src/emacs/lean-util.el | 15 +++++++------ src/frontends/lean/info_manager.cpp | 16 +++++++++++++- 7 files changed, 65 insertions(+), 32 deletions(-) diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index 466b4d57f3..6c2fd9922e 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -255,13 +255,11 @@ triggers a completion immediately." (lambda (&rest) (funcall callback nil))))) -(defun company-lean--findp-location (arg) - (lean-generate-tags) - (let ((tags-table-list (company-etags-buffer-table))) - (when (fboundp 'find-tag-noselect) - (save-excursion - (let ((buffer (find-tag-noselect arg))) - (cons buffer (with-current-buffer buffer (point)))))))) +; (defun company-lean--findp-location (arg cb) +; (lean-get-info-record-at-point +; (lambda (info-record) +; (if-let ((source-record (plist-get info-record :source))) +; (funcall cb (plist-get source-record :file) . (plist-get source-record :line)))))) (defun company-lean--findp-annotation (candidate) (let ((type (get-text-property 0 'type candidate))) @@ -294,7 +292,7 @@ triggers a completion immediately." (prefix (company-lean--findp-prefix)) (candidates (cons :async (lambda (cb) (company-lean--findp-candidates arg cb)))) (annotation (company-lean--findp-annotation arg)) - (location (company-lean--findp-location arg)) + ;(location (cons :async (lambda (cb) (company-lean--findp-location arg cb)))) (match (company-lean--findp-match arg)) (no-cache t) (require-match 'never) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 89a5a9fafa..66335857ed 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -46,10 +46,29 @@ (defun lean-get-info-record-at-point (cont) "Get info-record at the current point" (lean-server-sync) - (lean-server-send-command - (list :command "info" - :line (line-number-at-pos) - :column (lean-line-offset)) - (cl-function - (lambda (&key record) - (funcall cont record))))) + (let ((pos (lean-find-hname-beg))) + (lean-server-send-command + (list :command "info" + :line (line-number-at-pos pos) + :column (lean-line-offset pos)) + (cl-function + (lambda (&key record) + (funcall cont record)))))) + +(cl-defun lean-find-definition-cont (&key file line column) + (find-file file) + (goto-char (point-min)) + (forward-line (1- line)) + (forward-char column)) + + +(defun lean-find-definition () + "Jump to definition of thing at point" + (interactive) + (lean-get-info-record-at-point + (lambda (info-record) + (if-let ((source-record (plist-get info-record :source))) + (apply #'lean-find-definition-cont source-record) + (if-let ((id (plist-get info-record :full-id))) + (message "no source location available for %s" id) + (message "unknown thing at point")))))) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 8bbfba424b..276595d794 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -101,6 +101,7 @@ (local-set-key lean-keybinding-show-key 'quail-show-key) (local-set-key lean-keybinding-eval-cmd 'lean-eval-cmd) (local-set-key lean-keybinding-server-restart 'lean-server-restart) + (local-set-key lean-keybinding-find-definition 'lean-find-definition) (local-set-key lean-keybinding-tab-indent-or-complete 'lean-tab-indent-or-complete) (local-set-key lean-keybinding-lean-show-goal-at-pos 'lean-show-goal-at-pos) (local-set-key lean-keybinding-lean-show-id-keyword-info 'lean-show-id-keyword-info) @@ -125,6 +126,7 @@ ["Show type info" lean-show-type (and lean-eldoc-use eldoc-mode)] ["Show goal" lean-show-goal-at-pos t] ["Show id/keyword info" lean-show-id-keyword-info t] + ["Find definition at point" lean-find-definition t] ["Global tag search" lean-global-search t] "-----------------" ["Run flycheck" flycheck-compile (and lean-flycheck-use flycheck-mode)] diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index bb58cd6846..fee099eb14 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -152,6 +152,9 @@ false (nil)." (defcustom lean-keybinding-server-restart (kbd "C-c C-r") "Lean Keybinding for server-restart" :group 'lean-keybinding :type 'key-sequence) +(defcustom lean-keybinding-find-definition (kbd "M-.") + "Lean Keybinding for find-definition" + :group 'lean-keybinding :type 'key-sequence) (defcustom lean-keybinding-tab-indent-or-complete (kbd "TAB") "Lean Keybinding for tab-indent-or-complete" :group 'lean-keybinding :type 'key-sequence) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 990ae6be5d..424c3217c7 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -40,7 +40,7 @@ (cl-defun lean-info-record-to-string (info-record) "Given typeinfo, overload, and sym-name, compose information as a string." - (destructuring-bind (&key type overloads synth coercion proofstate full-id symbol extra) info-record + (destructuring-bind (&key type overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record (let (name-str type-str coercion-str extra-str proofstate-str overload-str stale-str str) (setq name-str (cond @@ -103,14 +103,10 @@ (defun lean-eldoc-documentation-function (&optional add-to-kill-ring) "Show information of lean expression at point if any" (interactive) - (cond ((or (and (not (looking-at (rx white))) - (not (eolp))) - (and (looking-back (rx (not white))) - (not (bolp)))) - (lean-get-info-record-at-point - (lambda (info-record) - (when info-record - (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))))))) + (lean-get-info-record-at-point + (lambda (info-record) + (when info-record + (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))))) (defun lean-show-type () "Show information of lean-expression at point if any." diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el index 5ffb550f8c..fdd7d2b39b 100644 --- a/src/emacs/lean-util.el +++ b/src/emacs/lean-util.el @@ -147,15 +147,16 @@ (when id-beg (buffer-substring id-beg cur-pos)))))) -(defun lean-line-offset () - "Return the byte-offset of current position, counting from the +(defun lean-line-offset (&optional pos) + "Return the byte-offset of `pos` or current position, counting from the beginning of the line" (interactive) - (let ((bol-pos - (save-excursion - (beginning-of-line) - (point))) - (pos (point))) + (let* ((pos (or pos (point))) + (bol-pos + (save-excursion + (goto-char pos) + (beginning-of-line) + (point)))) (- pos bol-pos))) (defun lean-whitespace-cleanup () diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index c8954b49e7..94bfc22797 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "library/choice.h" #include "library/scoped_ext.h" #include "library/pp_options.h" @@ -30,13 +31,26 @@ public: } }; +std::string olean_file_to_lean_file(std::string const & olean) { + lean_assert(is_olean_file(olean)); + std::string lean = olean; + lean.erase(lean.size() - std::string("olean").size(), 1); + return lean; +} + class identifier_info_data : public info_data_cell { name m_full_id; public: identifier_info_data(name const & full_id): m_full_id(full_id) {} - virtual void add_info(io_state_stream const &, json & record) const { + virtual void add_info(io_state_stream const & ios, json & record) const { record["full-id"] = m_full_id.to_string(); + if (auto olean = get_decl_olean(ios.get_environment(), m_full_id)) + record["source"]["file"] = olean_file_to_lean_file(*olean); + if (auto pos = get_decl_pos_info(ios.get_environment(), m_full_id)) { + record["source"]["line"] = pos->first; + record["source"]["column"] = pos->second; + } } };