coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
Chronological Thread
- From: Merlin Göttlinger <megoettlinger AT gmail.com>
- To: coq-club AT inria.fr
- Cc: Pierre Courtieu <pierre.courtieu AT gmail.com>
- Subject: Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
- Date: Fri, 13 Apr 2018 13:50:01 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f50.google.com
- Ironport-phdr: 9a23:yetRGBMGT+4hsA38cIkl6mtUPXoX/o7sNwtQ0KIMzox0Lfr/rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclRWS5ODIOyYYUMEuQPI/pXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQze2wIvAcgOsHDVrNXzLKgcUOatzLXUzTXHbvNW3zj955bSchs8pvyMWKx/ccXWyUYxCwPFklGQqY3jPzOayOsNqXOW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exFPc9Shh3oo5Odm1RFR4bNOkCpdcqTyWOoRsTs4iX21lvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5lea6/iwqr/UiuyuDwStO40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVnMEyPsmEj6kLeadkA+9eip7+TnbK/mppiZN4JsjwHxLKsumsuhDuQkLggOW2mb+eKz1LL95030W7pKjvgsnanYtJDWP9gUpqm8AwNNyIYs9w6/Dyu60NQfhXQIMFVFeAueg4f1P1HOPev3AOykg1WslTdr3+rJMqfgApXLNHjDka3ucaxz605Gm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxlsPqEtF80LQxx36TBq6fP67I+QuN6+0oLvWQYI4TtzvnA/cg7v/qy3Q+nAlOLuGSwZILZSXgTbxdKEKDbC+p249ZSDZYjk8FVOXvzWa6f3tWbne2Ubg742hiWo2jBIbHAIuqhe7YhXvpLthtfmlDT2u0PzLwbYzdAqUDbSuTJolqlTlWDeH8Gb9k7gmnsUrB85QiLufQ/XdF55fq1dww5vGL0B9vrXp7CMOS12zLRGZxzDsF
To add to that discussion:
I find this especially annoying using a tiling window manager where it reorders those windows due to newly opening the frames so that the main window with the code I just loaded becomes one of the smaller ones (because it is the oldest of the three) which in turn causes company-coq to remember that frame being to small to split. This then causes the documentation for the completions which I have automatically shown to be displayed in the *goal* frame so that I can't see the goals anymore.
Andrej Bauer <andrej.bauer AT andrej.com> schrieb am Fr., 13. Apr. 2018 um 15:34 Uhr:
> For the latter it would help to know in which scenario you need to restart coq.
Decativating coq because we're starting a fresh one in another buffer
is the common case when we don't want the existing frames to disappear
and re-appear.
- [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
- 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.