Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support collapsible trace nodes #35

Open
JLimperg opened this issue Mar 28, 2023 · 3 comments
Open

Support collapsible trace nodes #35

JLimperg opened this issue Mar 28, 2023 · 3 comments

Comments

@JLimperg
Copy link

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
Copy link
Contributor

Kha commented Mar 28, 2023

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
Copy link
Author

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

@Kha
Copy link
Contributor

Kha commented Mar 30, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants