[Matafou]

Coq: key bindings for all backends, and fixes in the goals and response buffers

• Script buffer: coq-mode-map is the keymap of Coq mode in every backend, and with Proof General it has priority over proof-mode-map. This is now documented in the manual and in CHANGES: users keep their key bindings when they switch backend by defining them in coq-mode-map.
• Goals and response buffers: they had their own copy of the default keys of the queries, so the key bindings of the user in coq-mode-map did not apply there, and each backend had to redo the copy.
  • The new list coq-all-buffers-commands names the commands of the script buffer that make sense in these buffers too: queries, display and printing options.
  • coq-all-buffers-keymap returns a keymap with the key bindings of these commands in coq-mode-map, both the default ones and those of the user. It does not include the keymaps that coq-mode-map inherits from. It also has C-c C-a C-r and C-c C-a C-g, which store the response and the goals (in the script buffer, these keys are insertions).
  • Proof General makes this keymap a parent of coq-goals-mode-map and coq-response-mode-map, before its generic keymaps. It rebuilds it each time these buffers are set up, so after the user's configuration. Key bindings the user put directly in these mode maps keep their priority.
  • The hypothesis keys (f, F, h, H) stay in the goals buffer only.
  • Change: C-c C-a C-r and C-c C-a C-g now also work in the goals buffer.
• Fix: storing the goals or the response again, for instance with C-c C-a C-r from response-freeze, opened a new frame each time. It now updates the visible window that already displays that buffer.
• Keys q and c of the goals and response buffers (bury-buffer, pg-response-clear-displays) never worked: they were bound to the event symbols [q] and [c] instead of characters. They are now commented out, with the working version and the question whether they are useful. No change of behavior.
• Tests, with and without Proof General: user key bindings and their priorities in the three buffers, the hypothesis keys only in the goals buffer, the generic Proof General keys still working, and storing twice opening a single frame.