search

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

Backport idris2-jump-to-def to idris-mode #593

Closed keram closed 1 year ago

keram commented 1 year ago

This is reminder for a missing feature from idris2-mode

https://github.com/idris-community/idris2-mode/commit/a37e19ec670f965943224cfb5719cca66fabf0eb https://github.com/idris-community/idris2-mode/commit/e0cd600154dbd576ba77eed03c754b7c1b55da21 https://github.com/idris-community/idris2-mode/commit/0f7c496c8fb9df9c05958f30e5633569a9b9e3a7

Unrelated but also probably to backport : https://github.com/idris-community/idris2-mode/commit/3ab0c023a9114a831ddde6821b1a08e8564df222 ( keyword highlight) https://github.com/idris-community/idris2-mode/commit/77390611a934f13e03a45e9f8a4e476dd17a9c5b (make-lemma and lidr)