make function for nvim coqtail output
- Enclose shortcut commands in function for nvim-coqtail - Add ghci/.ghci - Add gitignore
This commit is contained in:
parent
28e1589857
commit
39c4c3b609
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
|
@ -0,0 +1 @@
|
|||
*.sw[op]
|
3
ghci/.ghci
Normal file
3
ghci/.ghci
Normal file
|
@ -0,0 +1,3 @@
|
|||
-- From: https://github.com/tomtomjhj/dots/blob/master/.ghci
|
||||
|
||||
-- :set prompt "λ> "
|
1
ghci/README.md
Normal file
1
ghci/README.md
Normal file
|
@ -0,0 +1 @@
|
|||
Place `.ghci` in `$HOME`.
|
|
@ -13,17 +13,36 @@ source ~/.vimrc
|
|||
se nohls
|
||||
|
||||
" Allow pasting to system clipboard
|
||||
" Thanks to: ShougoShougo#neovim
|
||||
"" Thanks to: ShougoShougo#neovim
|
||||
if has('unnamedplus')
|
||||
set clipboard& clipboard+=unnamedplus
|
||||
else
|
||||
set clipboard& clipboard+=unnamed
|
||||
endif
|
||||
|
||||
" Coqtail stuff
|
||||
let @i=":CoqJumpToEnd | call append('.', ['(* -- AUTO OUTPUT (Info) --'] + getbufline(b:coqtail_panel_bufs['info'], 1, '$') + ['*)'])
"
|
||||
let @g=":CoqJumpToEnd | call append('.', ['(* -- AUTO OUTPUT (Goal) --'] + getbufline(b:coqtail_panel_bufs['goal'], 1, '$') + ['*)'])
"
|
||||
|
||||
" Emacs proofgeneral-like shortcuts for coqtail
|
||||
" 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
|
||||
|
|
Loading…
Reference in New Issue
Block a user