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: Andrej Bauer <andrej.bauer AT andrej.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
- Date: Fri, 13 Apr 2018 10:55:32 +0200
- Authentication-results: mail3-smtp-sop.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-f169.google.com
- Ironport-phdr: 9a23:NjR7ihRdFYlhAfIIZ/HOmDE/QNpsv+yvbD5Q0YIujvd0So/mwa6ybBKN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRAAoy+YYsBD+QPM+VFoYfju1QDtge+CRW2Ce/z1jNEmn370Ksn2OohCwHG2wkgEsoSvXTSsdr1LrkdUeKox6TV1zrDcu1Z2S3g44XPaB8hp+yDXahufsrT00UgDBnKjkiOpoz/JD6azOINvHWB7+V+V+KjkXIoqwZ0ojW2wMonl4fHhoUQyl/e9CV5xp44KsO9SEFhfdGkC5VRtyCZN4t3WM8iRHtouCk8x7YbupC7ZDAHxIo7yxPbcfCKcIiF7gj9WOqPLzp0nm9pdbO7ihqq70Ss1vHwWtSx3VpXoSdIkMXAu3UD1xzd5MiLVv5w80Sv1DqT0g3e5PxILEA1mKfeMZEt3qM8m5QWvEveACD2lkD7jKGNeUo4/uWl7fnsbK/8qZ+GLYB0jxnzMqQwlcy7BuQ1Kg0OUHKa+eS4zbHj/Er5TKlTgv04j6XUsZTXKd4Upq6+BA9V3YIj5AilAzi619QYmGELLFNDeB2Zk4jkI0/CLOz8APulgFmhkC1ny+7YMrDvGJnBM3nOnbP5cbZ48UFcyQ4zzd5F55JTD7EMOOj8Wknsu9zCEBA5MRa4zP39B9VgyIweQ3mCDbWfMKzPq1+H+OAvL/OQa48SvTbxM+Il6OL2jX8lhV8derGk0ocQaHChB/hpP0GZYWf3jdoaCmcLvg8+TPTwh1GYUD5TYWyyX6Mm6T0hBoKmF9SLeof4q7uYlAy/A5ceMmtBExWHFWriX4SCQfYFLiyIdJxPiDsBAJGnR5Us11mEvRL30fIzJ+zY4CAa85jqydVvz+TVmQs/93p/CMHLgDLFdH19gm5dH2x+56t4u0Eojw7bifEp0cwdLsRa4rZyail/MJfdy+JgDNWrAFDIeNuTRVTgSdKjU2loEoABhuQWakM4IO2MywjZ1nPwUbYTm6aGBto/9aeOhyGsdfY48G7P0ewat3djQsZLMjf41Kt29gyWBomR1kvAyffseqMb0yrAsmyEyDjWsQ==
A partial solution is to store the frame configuration in a register
and then to restore it after Proof General moved the frames around:
https://www.emacswiki.org/emacs/FramesAndRegisters
It would still be better if Proof General just left the frames alone.
Let me look at the code...
- [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.