Stream: Proof General users

Topic: Switch Window Orientation


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Pierre Courtieu (Nov 04 2022 at 10:18):

This can also be configured via the coq menu.

view this post on Zulip Rudy Peterson (Nov 04 2022 at 19:37):

Thanks! I was able to find it in the coq menu!


Last updated: Feb 06 2023 at 07:03 UTC