ProofGeneral vs Agda keybindings

[mikeshulman]

Narya's Emacs mode is intended to be a hybrid of Coq-style (ProofGeneral) partial processing with Agda-style hole-filling. But this causes some conflicting expectations regarding keybindings.

In Agda, C-c C-b moves Backwards to the previous hole, just as C-c C-f moves Forwards to the next hole. In ProofGeneral, C-c C-b processes the entire buffer. I didn't want to clobber the default ProofGeneral bindings, so I decided to try C-c C-j and C-c C-k for moving between holes (j and k being used in some keyboard interfaces for down and up, respectively). But I still find myself accidentally hitting C-c C-b from time to time in narya-mode and unintentionally processing the whole buffer.

(In fact, personally I've never intentionally used C-c C-b even when working with Coq. If I want to process the entire buffer, it's just as easy to move to the end of the buffer with M-> and then process to point with C-c RET.)

Should Narya's ProofGeneral mode disable the default meaning of C-c C-b? Options I can think of, other than the current one, include:

1. Just disable C-c C-b without binding it to anything. Then someone who's used to it from ProofGeneral won't be surprised by having it do something different (but they'll have to do something else for what they meant, like M-> and C-c RET), while someone used to Agda won't accidentally process the entire buffer.
2. Wrap C-c C-b in a confirmation prompt "Do you want to process the entire buffer?" Then someone who's used to it from ProofGeneral will be able to get what they want with an extra keystroke, while someone used to Agda will be able to cancel their mistake before it processes the entire buffer.
3. Re-bind C-c C-b to move to the previous hole, as in Agda (and presumably also bind C-c C-f to move to the next hole). Then someone used to ProofGeneral will be surprised at the behavior (but at least it's only a cursor motion command, not something that causes processing), while someone used to Agda will experience familiar behavior.
4. Supply a customization option like narya-use-agda-keybindings that switches between two or more of these options depending on how it's set.

A similar story could be told about C-c C-r, which in ProofGeneral retracts the entire buffer, while in Agda it "refines" a hole. I haven't been bitten by that one, since Narya doesn't (yet) have an analogue of Agda's "refine".

A different question is about C-c C-n, which in ProofGeneral processes the next command, while in Agda it normalizes a term. We certainly can't do without that PG meaning, and it seems more important and more commonly used than normalizing a term. Another way to normalize a term in Narya is C-c C-v echo <TERM>, although once we have "hole regions" that won't automatically normalize the term in the current region.

Also it occurs to me that Narya's C-c C-t should really be C-c C-, to match the Agda meaning. Does anyone use Agda's C-c C-t and C-c C-e that show only the goal type or only the context without the other?