undo-tree

ZF on Agda の方の気まずいバグの方はなんとかなって、クラスと集合の違いに付いて理解が深まった。クラスは順序数方程式の解に上界がないんだな。

ingress の方は不義理してすみません。

なんですが、今日のお題は Emacs の undo-tree 。VSCode のAgdaはあんまり良くなかったので、いまだにEmacsなんですが、viper から evil に乗り換えました。

今は、emacs lisp の packager があって、emacs lisp 経由で install するらしい。

　　;; Set up package.el to work with MELPA
　　(if nil (progn
　　(require 'package)
　　(add-to-list 'package-archives
　　　　　　　　 '("melpa" . "https://melpa.org/packages/"))
　　(package-initialize)
　　(package-refresh-contents)

　　;; Download Evil
　　(unless (package-installed-p 'evil)
　　　(package-install 'evil))
　　))

一度、入れたら nil で切っておかないと、毎回、アクセスが...

evil は vim なので undo が複数回できる。別に Emacs 側のを使ってたので良いんですが、ところが、

　　undo-tree っての入れられて、undo が編集履歴の一つの枝に限定

げ。つまり、戻って再編集すると、その先に戻れない。そのためには C-X u で graphical (characterの) mode に入って枝を選択する必要がある。

こんなの。

|　　　　　　　　　　　　　　　　　　　　s
|　　　　　　　　　　　　　　　　　　　 __|
|　　　　　　　　　　　　　　　　　　　/　 \
|　　　　　　　　　　　　　　　　　　 o　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　/ \
|　　　　　　　　　　　　　　　　　 x　 o
|


この選択が良くわからなかったんですが、

　　C-f で切り替えた後に space を打つと、その枝が選択される

という方式らしい。なにそれ。ちゃんと help に書いといて。

Agda はかなり試行錯誤するので、普通に木をたどる方が便利な気がする。はずしてしまおうかどうか考え中です。