Hover for Help in Emacs Lisp
Borrowing a helpful feature from LSP-land to enhance Emacs Lisp mode
Lately I’ve been working on a Binary Decision Diagrams (BDD) library for Lean 4, which is a “programming language and theorem prover.” I’ve had some experience with similar so-called “proof assistants”, namely Agda and Coq, but I haven’t used Lean beforehand.
Lean 4 is a big project, and there’s a lot to learn for a n00b trying to become productive, and do it fast. As a Microsoft-backed project, Lean is very well integrated with VS Code, and so I hesitantly opted to step out of the comfort of Emacs and start my Lean journey using VS Code.
Now, editing in VS Code is a pain. I keep typing shortcuts that make no sense outside of Emacs and chasing after their unintended results. However, I found browsing unfamiliar Lean code with VS Code to be a rather nice experience. Since the keyboard shortcuts burnt into my muscle memory weren’t doing me any good, I got my hands off the homerow and on the trackpad, and started pointing and clicking around.
One of the features I found most attractive for browsing code is the info popup you get whenever you hover over an identifier with the mouse pointer. It helps you figure out what a construct does/means right there in the context where you encounter it, with minimal effort and distraction.
That led me to think about how Emacs, the “self-documenting editor”,
could also benefit from such a hover-for-help info popup. The Emacs
package lsp-ui
provides such a feature for programming languages
with appropriate LSP support, what I wanted was something similar but
for Emacs Lisp, since the flexibility of Lisp macros make it common
enough to stumble upon unknown macros while browsing Lisp code.
[ There’s also a package called eldoc-box
, inspired by lsp-ui
,
which does provide an info popup for Emacs Lisp, but it doesn’t work
with the mouse (only with the text cursor, or “point”) and it doesn’t
show the function’s documentation (only its signature). ]
Luckily, adding this feature for Emacs Lisp was easy enough with the infrastructure I already had in place in my experimental Emacs branch. Here’s how it looks so far:

This screencast shows a couple more of my improvements for Emacs’s Emacs Lisp editing mode:
- Semantic highlighting—how symbols look tell you what they mean.
- Auto-emphasize occurrences of the local variable at point.
For comparison, here’s how “vanilla” Emacs displays the same code:

These features are part of my “teaching Emacs some Lisp” effort, in which I venture to enhance Emacs’s support for editing its own configuration and implementation by leveraging semantic analysis. Other niceties include better completions, jumping to definitions/references of local variables, reliably renaming local variables… You can see these in action in the following screencast:
