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
- [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Merlin Göttlinger, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Gaëtan Gilbert, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
Archive powered by MHonArc 2.6.18.