Currently undo does not work well in the Emacs interface. Go for one of two options:

  • Either use the ordinary, textual Emacs undo facilities.
  • Or implement a proper, type-checking state sensitive undo facility.

Update: I fixed this (at least temporarily) by turning off the Agda-specific undo features. If you want the previous behaviour you have to set a customizable flag (M-x customize-variable agda2-undo-kind).

Page last modified on June 02, 2007, at 03:53 PM
Powered by PmWiki