idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Restore position after case split #583

Closed keram closed 1 year ago

keram commented 1 year ago

Addresses feedback on https://github.com/idris-hackers/idris-mode/pull/465 with small improvement for making case from hole where the point is moved back to position of _ in case _ of as that is place user may most likely edit next.

After change

output-2022-12-07-00:56:42

Closes https://github.com/idris-hackers/idris-mode/pull/465

jfdm commented 1 year ago

Rerunning the jobs as there is a issue with emacs and packages IIUC.

jfdm commented 1 year ago

yay, passing tests.