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

Close the command output when empty #374

Open
meithecatte opened this issue Nov 7, 2024 · 1 comment
Open

Close the command output when empty #374

meithecatte opened this issue Nov 7, 2024 · 1 comment

Comments

@meithecatte
Copy link

The command output window (on the bottom-right by default) tends to be empty a lot of the time, taking up valuable space, which can be an issue when dealing with larger proof contexts. I believe the user experience would be better if the command output window got hidden when empty, leaving 100% of the vertical space to the proof context.

@whonore
Copy link
Owner

whonore commented Nov 10, 2024

That seems like a reasonable feature to provide as an option. In the meantime, although it's not a perfect solution, you can already resize or even close the goal and info windows. You can also re-open them and partially reset their positions with :CoqRestorePanels.

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