Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone


Chronological Thread 
  • From: Andrej Bauer <andrej.bauer AT andrej.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
  • Date: Fri, 13 Apr 2018 10:34:22 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrej.bauer AT andrej.com; spf=None smtp.mailfrom=andrej.bauer AT andrej.com; spf=None smtp.helo=postmaster AT mail-io0-f180.google.com
  • Ironport-phdr: 9a23:Z228ghdV0hMEjplwoSZTMlWwlGMj4u6mDksu8pMizoh2WeGdxcS5bB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTy1BDIOyYYUMEuQPI/pXopLhp1cStxayGRWgCP/txzJOm3T43bc60+MkEQzewAEgGc8BsG7Ko9X3KawfTPq6zLTWwjXZcvhb3i3y6I7VfRA7v/6MX6h8ftHLxkkyCQzFlE6dppbjPzyIzOQCrWqb4/B8WuKojm4qsgd8qSWsyMc0koTFmJ4Zx1Te+Sh6wIs5P8O0RFB1bNK+DZddtD2WO5NoTs8+X21kpSM3xqAJtJO5YCQHzZonxxDRa/CbdoWF4RzuWPqULDp2mX5oeLOyihOo/kS81+HxWMy530tUoSpLl9TMuGsC2ADX58WBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M5x74/jJsTsUDaEi/3n0X6kLaadks59uWr9+jreLrmppibN497jgHxLL4ildC4AeQ9KgQOXm6b9vqg1LD740H1XLFHguc1n6TZqpzWO9oXq6CjDwNI0Ysv9w6zDzK839QZmXkHIkhFeBWCj4XxIV7OJu33De2hjFSuijtk3OrJPqD/DZXXNXXMirHhcqtn60FCygo/18xQ55VRCr0ZOvL8RlfxtMDEDh8+KwG73+HnCMxk2owCXWKPH7SWPbjJsV6I4+IvO/ODaJUUuDb7Mfgl5uThgWU3mV8HLuGV2s48b2nwNfB7KQ3Nan31x9wFDG0ivwwkTeWshkfUAhBJYHPndqQw/Dw5QKivEIrZDtSkhrCb0SX9FJRLa3puA1aAC3rqMY6DXqFfO2qpPsZ9n2lcBvCaQIg72ETr7Veikus1Hq/v4iQd8Knb+p1w7uzXmws18GUuXc2b33uATSd/mWZaH2ZqjpA6mlR0zxK46YY9m+ZRTIYB7vVFSAo4c5Xbyr4iUo2gakf6Zt6MDW2ebJCmDDU2FIxjxtYPZwN8HI3ngEmTh2ylBLgak7HND5sxoPrR

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



Archive powered by MHonArc 2.6.18.

Top of Page