diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index bf4a712b3..b9b3c6504 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -105,6 +105,7 @@ ["Show type info" lean-eldoc-documentation-function lean-eldoc-use] ["Fill a placeholder" lean-fill-placeholder (looking-at (rx symbol-start "_"))] ["Find tag at point" lean-find-tag t] + ["Global tag search" lean-global-search t] "-----------------" ["Run flycheck" flycheck-compile lean-flycheck-use] ["List of errors" flycheck-list-errors lean-flycheck-use] diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el index 1426a9c57..cc46bfd28 100644 --- a/src/emacs/lean-tags.el +++ b/src/emacs/lean-tags.el @@ -8,6 +8,8 @@ (require 'f) (require 'lean-util) +(defalias 'lean-global-search 'tags-apropos) + (defun lean-tags-table-list () (-filter 'f-exists? (--map (f-join it "TAGS") (lean-path-list))))