From c39055034007f9106ad41185ffe8525d240e0c34 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Thu, 30 Jul 2015 10:46:47 -0700 Subject: [PATCH] feat(emacs/lean-mode.el): add show-goal-at-pos and show-id-keyword-info in the menu --- src/emacs/lean-mode.el | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 9283a2827..e611dc44c 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -227,6 +227,8 @@ placeholder, call lean-server with --hole option, otherwise call ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))] "-----------------" ["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] ["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]