From 9161a6a2103475d0f9338206d990cf3f94dc6650 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 16 Sep 2014 23:57:46 -0700 Subject: [PATCH] fix(emacs/lean-type): change where to trigger eldoc Previously, eldoc is triggered regardless of current position. Now, it is triggered: - *NOT* looking-at whitespace or - looking-back end-parens such as ')', '}', ']', etc --- src/emacs/lean-server.el | 3 ++- src/emacs/lean-type.el | 6 +++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 6fa2d6e06..1f49b1be4 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -493,7 +493,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (defun lean-server-get-info-record-at-pos (body) (let* ((file-name (buffer-file-name)) (column (current-column))) - (when (and (looking-at (rx (or white "," ")" "}" "]"))) + (when (and (or (looking-at (rx (or white "," ")" "}" "]"))) + (eolp)) (> column 1)) (setq column (1- column))) (lean-info-record-parse body file-name column))) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 4b452f97a..58cf981b7 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -42,7 +42,11 @@ (defun lean-eldoc-documentation-function () "Show information of lean expression at point if any" (interactive) - (lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont)) + (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))) ;; ======================================================= ;; eval