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

Published 20 hours ago • verified publisher icon leanprover-community

Support collapsible trace nodes

Open JLimperg opened this issue 1 year ago • 3 comments

The option to collapse/expand trace nodes is extremely helpful when navigating e.g. typeclass synthesis traces. But at least with my setup (Doom Emacs + lean4-mode), the traces are always fully expanded with no option to collapse them. Could we get this capability as well?

JLimperg avatar Mar 28 '23 16:03 JLimperg

This would be great to have, but honestly I don't see anyone putting that much work into the Emacs mode, which would also feel like kind of a waste given the dearth of users. Probably the most realistic solution would be to get the entire HTML info view either inside or at least next to Emacs.

Kha avatar Mar 28 '23 16:03 Kha

Fair. Have you looked into any of the Emacs HTML modules? (Emacs Application Framework seems to be the most developed one.)

JLimperg avatar Mar 28 '23 19:03 JLimperg

I was only aware of the xwidget builtin that usually is not compiled in. EAF does look extensive, but also like a pain to install.

Kha avatar Mar 30 '23 08:03 Kha