lean4-mode icon indicating copy to clipboard operation
lean4-mode copied to clipboard

Hover docs in info view

Open ultronozm opened this issue 1 year ago • 0 comments

These are available in the fork https://github.com/ultronozm/lean4-mode and I would be happy to upstream them here once eglot is available here as an lsp backend.

There is the further issue of how best to achieve "recursive hovering". I've managed this crudely using the mini-package https://github.com/ultronozm/eldoc-icebox.el, together with a hook that sets up the Lean4 hover docs. I figure this can be discussed once the basic support is upstreamed.

ultronozm avatar Dec 05 '24 22:12 ultronozm