The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Why not ask https://github.com/ProofGeneral/PG/issues/ ?

There is variable  proof-shell-fiddle-frames which has a suspicious name 
but I don't know if that's what you want.

Gaëtan Gilbert

On 13/04/2018 10:34, Andrej Bauer wrote:
> I apologize for the triviality of this question, but I've just spent
> an hour reading manuals and the rest of the Internet. I can't be the
> only one trying to accomplish this.
>
> I am on Emacs 25.3 with the latest Proof-general from Homebrew (4.4_2 it 
> seems).
>
> I have to monitors and would like to place the *goal* and *response*
> buffers into separate windows on the second display. This is doable by
> setting
>
> * proof-three-window-enable to t
> * proof-multiple-frames-enable to t
> * proof-delete-empty-windows to nil
>
> I can manually position the *response* and *goal* frames where I want
> them to be.
>
> The problem is this: every time I kill Coq with C-c C-x, or I just
> switch to a new buffer and start a new coq session, Proof General
> moves the two frames back to the first display, on top of my existing
> Emacs buffer.
>
> Is there a way to tell Emacs to bloody leave the frames alone? I don't
> know of any other application with the audacity to move windows around
> without explicit user constent.
>
> The ideal solution would be to tell Emacs where specifically and of
> what size the two frames from *response* and *goal* should be.
>
> With kind regards,
>
> Andrej