Skip to content

Commit

Permalink
Call a user-specified hook function when defining keybindings
Browse files Browse the repository at this point in the history
This serves two purposes. First, it allows a user to define additional
keybindings for commands without removing the standard `<Leader>cXXX`
bindings. Second, it allows those bindings to be active specifically
in Coqtail-managed buffers.
  • Loading branch information
jesboat committed Feb 19, 2024
1 parent 92cd578 commit 3839207
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 0 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
27 changes: 27 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 <leader>ci <Plug>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 `<leader>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 <buffer> <S-Down> <Plug>CoqNext
imap <buffer> <S-Left> <Plug>CoqToLine
imap <buffer> <S-Up> <Plug>CoqUndo
nmap <buffer> <S-Down> <Plug>CoqNext
nmap <buffer> <S-Left> <Plug>CoqToLine
nmap <buffer> <S-Up> <Plug>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 (`<leader>cj`, etc) would remain active.

### Coq Executable

By default Coqtail uses the first `coq(ide)top(.opt)` found in your `PATH`.
Expand Down
4 changes: 4 additions & 0 deletions autoload/coqtail.vim
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 3839207

Please sign in to comment.