michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-mode.el): add show-goal-at-pos and show-id-keyword-info in the menu

Browse source
This commit is contained in:
Soonho Kong 2015-07-30 10:46:47 -07:00
parent 46a79ec43d
commit c390550340
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-mode.el
View file

@ -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]