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
This commit is contained in:
parent
9a2f1ba423
commit
9161a6a210
2 changed files with 7 additions and 2 deletions
|
@ -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)))
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue