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

feat(emacs/lean-mode.el): add lean-show-id-keyword-info

Browse source 
close #756
This commit is contained in:
Soonho Kong 2015-07-30 10:46:10 -07:00
parent 698b368f01
commit 46a79ec43d
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -158,6 +158,13 @@ placeholder, call lean-server with --hole option, otherwise call
(lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
(t
(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))
(defun lean-show-id-keyword-info ()
"Show ID/Keyword Information at the position"
(interactive)
(lean-exec-at-pos
"lean-print-id-keyword-info"
"*Lean Print*"
"--info"))
(defun lean-std-exe ()
(interactive)
@ -200,7 +207,9 @@ placeholder, call lean-server with --hole option, otherwise call
(local-set-key "\C-c\C-r" 'lean-server-restart-process)
(local-set-key "\M-." 'lean-find-tag)
(local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)
(lean-define-key-binding "\C-c\C-g" '(lean-show-goal-at-pos)))
(local-set-key "\C-c\C-g" 'lean-show-goal-at-pos)
(local-set-key "\C-c\C-p" 'lean-show-id-keyword-info)
)
(defun lean-define-key-binding (key cmd)
(local-set-key key `(lambda () (interactive) ,cmd)))