How to control emacs to split window when interpret Coq

Question

I am studing Coq with emacs. I spilt the emacs window vertically, the left is document and the right is code editing area. when I interpret Coq program, the result will show in the left window and cover the document. This bothers me. Whether there is such a way that I can split the code editing area horizontally and the interpreted result is shown in the bottom right?

Answer 1

By "code editing area" do you mean the "goal buffer"? If so, what you describe sounds like what would happen using the default settings. Try resetting all settings and make sure that you are using "three pane mode" and proof-layout-windows is set to either "smart" or "hybrid".

Answer 2

After you invoke the 3 Windows mode, you can customize its layout manually without being disturbed by Proof General.

Here are some shortcuts that might help:

• C-x 5 2 creates a new frame (container of windows), which is quite useful if you are working on multiple displays.
• C-x 2 creates a new window below (similar to :split in Vim)
• C-x 3 creates a new window on right (similar to :vsplit)