Commit 394b8fc3 authored by Manu Beffara's avatar Manu Beffara
Browse files

Added visual and motion mappings for queries.

parent b4c2bf2e
......@@ -1426,6 +1426,32 @@ function s:coq.query_return (d) abort
" == Queries == {{{2
" Send a Query command made from the text of the current selection. The first
" argument is the current mode (see :map-operator in the Vim documentation)
" and the second argument is a printf template for the query.
function! s:operator (mode, format)
let range = [getpos("'[")[1:2], getpos("']")[1:2]]
call b:coq.query(printf(a:format, s:range_text(range)))
" The following functions are 'operatorfunc's for particular queries.
function! s:op_about (mode)
call s:operator(a:mode, 'About %s.')
function! s:op_check (mode)
call s:operator(a:mode, 'Check %s.')
function! s:op_search_about (mode)
call s:operator(a:mode, 'SearchAbout %s.')
" == Commands and mappings == {{{2
function! coqtop#Start () abort
......@@ -1444,6 +1470,13 @@ function! coqtop#Start () abort
inoremap <buffer> <silent> <C-Up> <C-\><C-o>:CoqRewind<CR>
inoremap <buffer> <silent> <C-Right> <C-\><C-o>:CoqToCursor<CR>
nnoremap <buffer> <silent> <localleader>a :set opfunc=<sid>op_about<cr>g@
vnoremap <buffer> <silent> <localleader>a :<C-U>call <sid>op_about(visualmode())<cr>
nnoremap <buffer> <silent> <localleader>c :set opfunc=<sid>op_check<cr>g@
vnoremap <buffer> <silent> <localleader>c :<C-U>call <sid>op_check(visualmode())<cr>
nnoremap <buffer> <silent> <localleader>s :set opfunc=<sid>op_search_about<cr>g@
vnoremap <buffer> <silent> <localleader>s :<C-U>call <sid>op_search_about(visualmode())<cr>
if b:coq.debugging
nnoremap <buffer> K :CoqQuit<CR>
nnoremap <buffer> C :message clear<CR>
......@@ -1469,6 +1502,13 @@ function! coqtop#Quit () abort
iunmap <buffer> <C-Right>
iunmap <buffer> <C-Up>
nunmap <buffer> <localleader>a
vunmap <buffer> <localleader>a
nunmap <buffer> <localleader>c
vunmap <buffer> <localleader>c
nunmap <buffer> <localleader>s
vunmap <buffer> <localleader>s
unlet b:coq
......@@ -139,6 +139,25 @@ Vim while Coq is processing sentences.
However, editing in a previously checked zone currently does not rewind
The following key mappings are used to send queries to Coq in the current
state. For instance, assuming <localleader> is ",", the command ",aiw" in
normal mode will display information about the word under the cursor in the
Infos window and ",ci(" will type check the contents of the current
Send a query "About {text}" for the selected text.
Send a query "Check {text}" for the selected text.
Send a query "SearchAbout {text}" for the selected text.
4. Configuration *coq-config*
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment