EAGLE 雑記 このページをアンテナに追加 RSSフィード

Sun May 15, 2011

[][] coqtop を Vim の中で動かして連携させる

プログラミング Coq を読んでいたらいつのまにかそんなかんじのを書いていた.どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います.

https://github.com/eagletmt/coqtop-vim

最新の vimproc を先にインストールしておく必要がある.


使い方としてはまず :CoqStart で coqtop からの出力を表示するバッファとウィンドウを作る.

f:id:eagletmt:20110516014942j:image

コードを書いていき,インサートモードで <C-g> するとその行まで coqtop に送られる.ノーマルモードで :CoqGoto あるいは <LocalLeader>g *1でも同じ.

f:id:eagletmt:20110516014943j:image

既に送られた領域の最後の行は Folded で色付けされ,これより上の行は編集できなくなる.

(ところで「編集できなく」するために今は CursorMoved,CursorMovedI でカーソル行をチェックして 'modifiable' を変更する,という方法でやっているけど,ある領域だけ完全に編集不可能にする方法はあるんだろうか.現状の実装だと undo とか setline() とかで簡単に編集されてしまう.編集されると :CoqGoto による巻き戻しが破綻する.)


一度送ってしまったけれども間違えたと思ってやり直したいときは,

f:id:eagletmt:20110516014944j:image

戻りたい行にカーソルを合わせて :CoqGoto あるいは <LocalLeader>g で,その行まで巻き戻される.

f:id:eagletmt:20110516014946j:image


coqtop が受け付けるコマンドの一部も Vim のコマンドとして提供している.

今はとりあえず

  • :CoqPrint (Print に相当)
  • :CoqSearchAbout (SearchAbout に相当)

が使える.

f:id:eagletmt:20110516014947j:image

f:id:eagletmt:20110516014945j:image

まだ安定性に不安が残るので,もしなにか挙動がおかしくなってきたら :CoqClear または <LocalLeader>c でクリアしてください.

*1:<LocalLeader> はデフォルトでは \ だと思う.詳細は :help maplocalleader で

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/eagletmt/20110515/1305479711