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

fix(emacs/lean-type): disable eldoc at flycheck error/warning

Browse source 
fix #204
This commit is contained in:
Soonho Kong 2014-09-20 10:18:43 -07:00
parent b429b961e6
commit ee4255eb3d
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -42,11 +42,15 @@
(defun lean-eldoc-documentation-function ()
"Show information of lean expression at point if any"
(interactive)
(when (or (and (not (looking-at (rx white)))
(not (eolp)))
(and (looking-back (rx (not white)))
(not (bolp))))
(lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont)))
(cond ((and lean-flycheck-use
(or (get-char-property (point) 'flycheck-error)
(get-char-property (point) 'flycheck-warning)))
nil)
((or (and (not (looking-at (rx white)))
(not (eolp)))
(and (looking-back (rx (not white)))
(not (bolp))))
(lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont))))
;; =======================================================
;; eval