Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

add language idris #2971

Merged
merged 1 commit into from
Jul 5, 2022
Merged

add language idris #2971

merged 1 commit into from
Jul 5, 2022

Conversation

mtoohey31
Copy link
Contributor

This pull request adds support for the Idris2 language. No grammar is included yet because I don't believe there is one (but I'm happy to be proven wrong if someone is able to find one). The only repo I could find was this one, but it's incomplete.

I have tested the language server and it works without issues.

The only thing I was unsure about is whether the filetype should be called idris or idris2, since there are breaking changes between the two languages. I lean towards idris, because:

  • files of both types share the .idr extension, so we couldn't really support both even if we wanted to since there's no simple way to distinguish between the languages
  • Idris 1 is not actively maintained

Copy link
Member

@archseer archseer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I think that's fine, we can always rename it in the future if needed

@archseer archseer merged commit d78354c into helix-editor:master Jul 5, 2022
@mtoohey31 mtoohey31 deleted the feat/idris branch December 10, 2022 17:02
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants