Add support for Emacs 28's repeat-mode
for working with Holes
#6548
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Emacs 28 has a global minor mode called
repeat-mode
that allows commands to define temporary keymaps that should be enabled right after the command was invoked. One example:other-window
(C-x o) can be repeated with a single o, without the C-x prefix when the mode is enabled.I proposed adding some basic support for Agda-mode as well. The commands are defined in
agda2-movement-repeat-map
and the keys are just abbreviations of the default bindings. This means that ifrepeat-mode
is enabled, you can now step through the holes in a file by just pressing C-f. I have currently implemented it in a way that you can switch back and forth between navigation, manipulation (case, refining, give) and querying. If this is not considered to be a good idea, we can also split it up into disjunct repeat maps.This was initially unintentionally incorrectly part of #6536, but I have adjusted that pull request and extracted the changes into this one.