Rudy Peterson (Nov 03 2022 at 18:33): Rudy Peterson (Nov 03 2022 at 18:33):Hello!
When I begin stepping through a coq file the goal window opens to the right of the file window.
How does one configure emacs to display the goal window below the file window?
I tried using the transpose frames but it messes with proof general and other coq settings such as prettifying symbols.
Can I configure my .emacs file to handle this?
Thanks!
Pierre Courtieu (Nov 04 2022 at 10:16):You can definitely rearrange your windows once the scripting started. But you will probably need to do it again for each new file you script. So you should probably use a predefined display mode: vertical/horizontal/hybrid /smart. Citing doc(https://proofgeneral.github.io/doc/master/userman/Customizing-Proof-General/#Display-customization)
If you want to force one of the layouts, you can set variable ‘proof-three-window-mode-policy’ to 'vertical, 'horizontal or 'hybrid. The default value is 'smart which sets the automatic behaviour described above.
Pierre Courtieu (Nov 04 2022 at 10:18):This can also be configured via the coq menu.
Rudy Peterson (Nov 04 2022 at 19:37):Thanks! I was able to find it in the coq menu!
Last updated: Oct 13 2024 at 01:02 UTC