diff --git a/CHANGELOG.md b/CHANGELOG.md index 2a539957..7f8d84c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,7 @@ ### Added - `g:coqtail_treat_stderr_as_warning` option to ignore unrecognized warnings on stderr. (PR #338) +- Add a hook for more flexible keybindings (PR #339) ### Fixed - Fix rendering of goals panel when no proof is active in Coq >= 8.16. diff --git a/README.md b/README.md index 2259c535..0cd7f762 100644 --- a/README.md +++ b/README.md @@ -99,12 +99,39 @@ The mappings above are set by default, but you can disable them all and define your own by setting `g:coqtail_nomap = 1` in your `.vimrc`. Some of the commands, such as `CoqNext`, also have insert-mode mappings by default, which can be disabled with `g:coqtail_noimap`. + Alternatively, you can keep the defaults but remap specific commands. For example, use `map ci CoqInterrupt` to avoid hijacking `CTRL-C`. +If a mapping for a command already exists when Coqtail is loaded, the default +mapping for that command won't be defined. + The `c` prefix may be inconvenient depending on your `mapleader` setting. In that case you can set a custom prefix with `g:coqtail_map_prefix` (or `g:coqtail_imap_prefix` for just insert-mode mappings). +Finally, after defining the standard keybindings, Coqtail will call a vim +function named `CoqtailHookDefineMappings` (if one is defined). This makes it +easy to add additional mappings without removing the standard mappings, and +to add mappings which are only active in Coqtail-managed buffers. One way to +use this hook is to make bindings for commands which augment the standard +Coqtail bindings instead of replacing them. One concrete example is: + +```vim +function CoqtailHookDefineMappings() + imap CoqNext + imap CoqToLine + imap CoqUndo + nmap CoqNext + nmap CoqToLine + nmap CoqUndo +endfunction +``` + +Adding that snippet to your `.vimrc` would create new bindings for `CoqNext`, +`CoqToLine`, and `CoqUndo`. Those bindings would be active in all Coq buffers, +including Coqtail panels, but inactive in other buffers. The standard Coqtail +bindings (`cj`, etc) would remain active. + ### Coq Executable By default Coqtail uses the first `coq(ide)top(.opt)` found in your `PATH`. diff --git a/autoload/coqtail.vim b/autoload/coqtail.vim index 0998420a..f164ba17 100644 --- a/autoload/coqtail.vim +++ b/autoload/coqtail.vim @@ -596,6 +596,10 @@ function! coqtail#define_mappings() abort endif endfor endfor + + if exists('*CoqtailHookDefineMappings') + call CoqtailHookDefineMappings() + endif endfunction " Initialize buffer local variables, commands, and mappings.