--- Day changed Fri Jun 09 2017
Nik05I just started to use agda and emacs and I got a small question. If I refine or do a case split, how could I undo such action?09/06 20:52
dolioDoes C-x u work?09/06 20:52
Nik05dolio and what if it wasnt the most recent change I did?09/06 20:54
dolioI don't know of a way to revert only one thing arbitrarily far back in the undo state. I don't think most editors allow that sort of thing.09/06 20:55
dolioI mean, you can repeatedly C-x u to undo all the way back.09/06 20:55
Nik05How could I change a hole back to a ? ?09/06 20:56
dolioUndo seems to do that, too, for me.09/06 20:57
Nik05thank you for helping out dolio09/06 21:11
dolioNo problem.09/06 21:12
mieteksometimes you have to undo twice to change back to ?09/06 22:26
mieteksometimes the emacs undo buffer gets confused if you try to undo very far back09/06 22:26
mietekbut it mostly works fine, both undo and redo09/06 22:26
mieteksometimes it’s easier to disable the "live" mode09/06 22:27
mietekC-c C-x C-d, I think?09/06 22:27
mietekedit the "dead" text, and C-c C-l again09/06 22:27
mietekwhen emacs is being particularly unhelpful about the holes/sheds09/06 22:27

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!