2021-05-01 01:45:52 +00:00
|
|
|
" Plugins will be downloaded under the specified directory.
|
|
|
|
|
call plug#begin('~/.config/nvim/plugged')
|
|
|
|
|
|
|
|
|
|
" Make sure you use single quotes
|
|
|
|
|
Plug 'whonore/Coqtail'
|
2021-07-29 06:47:34 +00:00
|
|
|
"Plug 'joom/latex-unicoder.vim'
|
2021-05-01 01:45:52 +00:00
|
|
|
|
|
|
|
|
" Initialize plugin system
|
|
|
|
|
call plug#end()
|
|
|
|
|
|
|
|
|
|
source ~/.vimrc
|
2021-07-15 07:15:40 +00:00
|
|
|
|
2021-07-29 06:47:34 +00:00
|
|
|
se nohls
|
|
|
|
|
|
2021-09-07 02:14:20 +00:00
|
|
|
" Allow pasting to system clipboard
|
2021-09-10 10:45:17 +00:00
|
|
|
"" Thanks to: ShougoShougo#neovim
|
2021-09-07 02:14:20 +00:00
|
|
|
if has('unnamedplus')
|
|
|
|
|
set clipboard& clipboard+=unnamedplus
|
|
|
|
|
else
|
|
|
|
|
set clipboard& clipboard+=unnamed
|
|
|
|
|
endif
|
|
|
|
|
|
2021-09-10 10:45:17 +00:00
|
|
|
|
2021-07-15 07:15:40 +00:00
|
|
|
" Coqtail stuff
|
2021-09-07 02:14:20 +00:00
|
|
|
|
2021-09-10 10:45:17 +00:00
|
|
|
"" Insert coq output as comment
|
|
|
|
|
function! InsertOutput(buffer)
|
|
|
|
|
" Position cursor after last executed line
|
|
|
|
|
CoqJumpToEnd
|
|
|
|
|
|
|
|
|
|
" Get Info/Goal buffer contents
|
|
|
|
|
let instrlst = getbufline(b:coqtail_panel_bufs[tolower(a:buffer)], 1, '$')
|
|
|
|
|
|
|
|
|
|
" Make comment to output
|
|
|
|
|
let outstrlst = ['(*', '#+BEGIN_OUTPUT (' . a:buffer . ')']
|
|
|
|
|
\ + instrlst[:-2] + ['#+END_OUTPUT (' . a:buffer . ') *)']
|
|
|
|
|
|
|
|
|
|
" Add comment to file
|
|
|
|
|
call append('.', outstrlst)
|
|
|
|
|
endfunction
|
|
|
|
|
|
|
|
|
|
let @i = ":call InsertOutput('Info')
"
|
|
|
|
|
let @g = ":call InsertOutput('Goal')
"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
"" Emacs proofgeneral-like shortcuts for coqtail
|
2021-09-07 02:14:20 +00:00
|
|
|
noremap <C-n> :CoqNext<CR>hh " next line. Dunno why cursor advaces horizontally 2 chars.
|
|
|
|
|
noremap <C-p> :CoqUndo<CR>hh " undo last line
|
2022-01-19 08:42:42 +00:00
|
|
|
|
|
|
|
|
"" Don't auto indent an extra level for branches
|
|
|
|
|
let g:coqtail_inductive_shift = 0
|
