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

[ new ] intro command - backport from idris2-mode #578

Closed keram closed 1 year ago

keram commented 1 year ago

https://github.com/idris-community/idris2-mode/pull/21

Updated with suggested key binding by Ohad

keram commented 1 year ago

Short update: trying to figure out good strategy for backward compatible key bindings and making new commands visible only on version that support it. Something like defining version specific key binding run time when we know what idris-protocol version user is running.

jfdm commented 1 year ago

trying to figure out good strategy for backward compatible key bindings and making new commands visible only on version that support it.

This would be good, but I think can be done separately to this PR. We have existing menu items (that are Idris2 specific) that are labelled. In the long run the menu should be dynamic (if that is possible), but otherwise let us do the bare minimum for a viable product.

keram commented 1 year ago

Added one simple test for idris-refine. The Idris2 workflow CI failures are unrelated, probably something went wrong with the build and cache as same code passes on fork actions https://github.com/keram/idris-mode/actions/workflows/idris2.yml