coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Context menu in Proof General

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Context menu in Proof General
Date: Sat, 25 Feb 2017 09:48:54 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:Jrg9tB3fpSYm6RFZsmDT+DRfVm0co7zxezQtwd8Zse0XLfad9pjvdHbS+e9qxAeQG96KtrQe0aGO7OjJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhDexe61+IAu5oQnNtMQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28dYsPCO8BMP5GoYn9vVwOqgOxCgqtBOPqzz9HmGX23agg3OQnFwHNwQstH84OsHvKq9X5LqYTUeGwzKnNzDXOdPxW2TLn54jJdhAtu+2DXbV1ccfIz0QkCgDLjk2IpID7Iz+Y0v4Bvmub4uZ6S+6jlXIrpxtsrjWs2MshjJTCiJgPxVDe7yp5xZ44Jd2mR05/Zt6pCJ5QuDubN4tyW88iWmJotDojxr0IpJK2fzYGxI4oxx7YbPyHfIyI7Qz5WOmNJjd4gWppeLO5hxms7Uit0vPwWtWw3VpQrSdIksPAum4T2xDP8MSLV/hw8lm51TaKzQ/T6+VEIU4ularcLp4s2qIwlpoNvkTEBCP3mUT2jKqTdkUl4eWo5OHnba/npp+YLYN7lgb+MqE2lsylHes4KhQOX3Sc+emkyLLj+lT5TKxWgf0yj6nWq4vXJd8bp668Gw9ayJwv6xe5Dze80dQXh2MLLFxfeEHPs4+8MFbXZfv8EP2XglK2kT4tyeqVEKfmB8DxLvnEp4XgeLNw8UtVzgx7mcxf6pUSGLAEJfPbVUr4tdieBRg8ZV/ni937Aclwg9tNEVmEBbWUZfvf

Not only I don't use it but I sometimes get bitten by it (inadvertently calling Hide through some keyboard shortcut).
The only Show/Hide facility that I use is the one provided by Company-Coq.

Théo

Le ven. 24 févr. 2017 22:59, Paul A. Steckler <steck AT stecksoft.com> a écrit :

In Proof General, do you use the Show/Hide context menu? If so, do you
use it to hide individual items, like tactic calls, or Notation
declarations, or do you use to hide chunks, like proofs and sections?

I'm working on a new version of Proof General, and I can get some
speedup if I can avoid creating some of those context menus, so I'd
like to get some sense of how this feature is used.

-- Paul

[Coq-Club] Context menu in Proof General, Paul A. Steckler, 02/24/2017
- Re: [Coq-Club] Context menu in Proof General, Théo Zimmermann, 02/25/2017
  - Re: [Coq-Club] Context menu in Proof General, Paul A. Steckler, 02/27/2017