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

feat(src/lean-mode.el): add 'configuration' menu and add toggle option for 'Show type at point'

Browse source 
close #456
This commit is contained in:
Soonho Kong 2015-03-05 14:33:57 -05:00
parent 039afb4578
commit b7c852a5c8
2 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -107,7 +107,7 @@
["Execute lean" lean-execute t]
["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
"-----------------"
["Show type info" lean-eldoc-documentation-function lean-eldoc-use]
["Show type info" lean-show-type 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]
@ -119,6 +119,9 @@
["Kill lean process" lean-server-kill-process t]
["Restart lean process" lean-server-restart-process t]
"-----------------"
("Configuration"
["Show type at point" lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
"-----------------"
["Customize lean-mode" (customize-group 'lean) t]))
(defconst lean-hooks-alist

7
src/emacs/lean-type.el
View file

@ -16,6 +16,13 @@
(require 'lean-debug)
(require 'flymake)
(defun lean-toggle-eldoc-mode ()
"Toggle eldoc-mode"
(interactive)
(cond
(eldoc-mode (eldoc-mode -1))
(t (eldoc-mode 1))))
(defun lean-fill-placeholder-cont (info-record)
"Continuation for lean-fill-placeholder"
(let ((synth (and info-record (cl-first (lean-info-record-synth info-record)))))