-
-
Notifications
You must be signed in to change notification settings - Fork 2.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add support for Agda #8285
Add support for Agda #8285
Conversation
This PR is ready for review. I may have a follow-up sometime adding proper function highlighting & als support, the former appears to be a legitimate upstream bug and the latter still a mystery. @the-mikedavis can you squash merge this or would you prefer me to rebase? |
We can squash + merge this, no need to rebase |
Is this stalling? |
It's done on my end, I've been running it locally for a while. The syntax highlighting is unfortunately pretty terrible - but it's nothing that can be addressed until tree-sitter/tree-sitter#880 is addressed. Any more specificity with regard to types kills performance exponentially (> 3 ish is unusable) and breaks highlighting for nested types above a certain level. |
Do you use it regularly and would you advise others to do so aswell? @omentic |
I mean, it's fine, it looks just like the above picture. I do not write Agda regularly in Helix and I would not advise others to do so as well because Helix lacks support for Unicode input, and Unicode input is required to write Agda. When a snippets system lands, it'd be fine, I guess: but without a "proof assistant mode" or similar not great. |
This needs co flicts resolved before being g merged |
267ebf1
(tangential re: a proof assistant mode: it's very likely it could piggyback off of debug mode, before or after a redesign. i've had no time to poke around and prototype something, unfortunately, but might in the far future...) |
* agda language support (wip) * improve highlights * disable agda-language-server * minor addendum to documentation * cargo xtask docgen * oh i can just do this neat * minor comment cleanup * upstream updated * imports: missed a spot --------- Co-authored-by: Michael Davis <[email protected]>
* agda language support (wip) * improve highlights * disable agda-language-server * minor addendum to documentation * cargo xtask docgen * oh i can just do this neat * minor comment cleanup * upstream updated * imports: missed a spot --------- Co-authored-by: Michael Davis <[email protected]>
* agda language support (wip) * improve highlights * disable agda-language-server * minor addendum to documentation * cargo xtask docgen * oh i can just do this neat * minor comment cleanup * upstream updated * imports: missed a spot --------- Co-authored-by: Michael Davis <[email protected]>
* agda language support (wip) * improve highlights * disable agda-language-server * minor addendum to documentation * cargo xtask docgen * oh i can just do this neat * minor comment cleanup * upstream updated * imports: missed a spot --------- Co-authored-by: Michael Davis <[email protected]>
supersedes #3092
todo:
(expr (expr (expr... (atom) @type)))