coqtop を Vim の中で動かして連携させる
http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた．どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います．
https://github.com/eagletmt/coqtop-vim
最新の vimproc を先にインストールしておく必要がある．
使い方としてはまず :CoqStart で coqtop からの出力を表示するバッファとウィンドウを作る．
コードを書いていき，インサートモードで
既に送られた領域の最後の行は Folded で色付けされ，これより上の行は編集できなくなる．
(ところで「編集できなく」するために今は CursorMoved,CursorMovedI でカーソル行をチェックして 'modifiable' を変更する，という方法でやっているけど，ある領域だけ完全に編集不可能にする方法はあるんだろうか．現状の実装だと undo とか setline() とかで簡単に編集されてしまう．編集されると :CoqGoto による巻き戻しが破綻する．)
一度送ってしまったけれども間違えたと思ってやり直したいときは，
戻りたい行にカーソルを合わせて :CoqGoto あるいは
coqtop が受け付けるコマンドの一部も Vim のコマンドとして提供している．
今はとりあえず
- :CoqPrint (Print に相当)
- :CoqSearchAbout (SearchAbout に相当)
が使える．
まだ安定性に不安が残るので，もしなにか挙動がおかしくなってきたら :CoqClear または
*1:
