The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Yes, I just found out about proof-shell-fiddle-frames, which still
doesn't seem to do what needs to be done, see

https://github.com/ProofGeneral/PG/blob/5d7c77ae029de273724248105f416d57983631b2/BUGS#L38

I think there is a further problem: when the Coq process is killed,
the associated bufferes are killed, and then the associated frames are
killed.

I'll open an issue.




On Fri, Apr 13, 2018 at 10:57 AM, Gaëtan Gilbert
<gaetan.gilbert AT skyskimmer.net>
 wrote:
> 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
>>
>