search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
64 stars 28 forks source link

Support collapsible trace nodes #35

Open JLimperg opened 1 year ago

JLimperg commented 1 year ago

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?

Kha commented 1 year ago

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.

JLimperg commented 1 year ago

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

Kha commented 1 year ago

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.