ssreflect の proof script のインデント

ssreflect を使っているとき，proofgeneral のデフォルトのままだと（といっても何が本当にデフォルトなのか把握できていませんが，少なくともそんなにいじってないはずの手元の環境では）インデントがあんまりうまくいってない感じが強いので何とかできないかなと思っています。

今日ちょっと coq-smie-indent.el などを見てみたら，by のインデントの調整くらいはすぐにできそうな気がしたのでやってみました。

(defadvice coq-smie-rules (around ssr-by-tactical (kind token) activate)
  (if (and (eq kind :before) (equal token "by")
           (save-excursion
             (skip-chars-backward "\t\n\r ")
             (= (char-before (point))  ?.)))
      (smie-rule-parent)
    ad-do-it))

by はデフォルトではインデントを深くするので，例えば

have -> : 1 + 1 = 2
  by reflexivity.

みたいになります。これはいいのですが，ssreflect では by を先頭に書くこともあって，例えば手元にある適当なコードを貼り付けますが

case.
move => H; move : (eq_sigT_snd H).
by rewrite eq_axiomK.

のようにも書きます。こういうときはインデントを深くしてほしくないので，advice でむりやりそうなるようにしました。

あとは => が tactical （と呼ぶのが正しいのかどうかいまいちわからないけど他に適切そうな言葉を知らない）として使われるときには ; より結合力が弱いはずなんだけどそういう動作になってないようです。

例えば，また適当に手元にあったものを貼り付けますが

by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *;
  match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.

みたいなのはデフォルトの動作だと

by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *;
                                                            match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.

となってとても残念。

これも何とかできるとよいなと思うのですが，こっちはたぶん文法規則を書き直す必要があるのでもっと面倒そう。