" Plugins will be downloaded under the specified directory.
call plug#begin('~/.config/nvim/plugged')

" Make sure you use single quotes
Plug 'whonore/Coqtail'
"Plug 'joom/latex-unicoder.vim'

" Initialize plugin system
call plug#end()

source ~/.vimrc

se nohls

" Allow pasting to system clipboard
"" Thanks to: ShougoShougo#neovim
if has('unnamedplus')
    set clipboard& clipboard+=unnamedplus
else
    set clipboard& clipboard+=unnamed
endif


" Coqtail stuff

"" 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
noremap <C-n> :CoqNext<CR>hh  " next line. Dunno why cursor advaces horizontally 2 chars.
noremap <C-p> :CoqUndo<CR>hh  " undo last line

"" Don't auto indent an extra level for branches
let g:coqtail_inductive_shift = 0