From ee4255eb3d7b00208519da91d275a35e2a2d5779 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Sat, 20 Sep 2014 10:18:43 -0700 Subject: [PATCH] fix(emacs/lean-type): disable eldoc at flycheck error/warning fix #204 --- src/emacs/lean-type.el | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 58cf981b75..cb24a00ea8 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -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