Skip to content
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

Update semantic highlighting code in line with the update IDE protocol #547

Merged
merged 4 commits into from
Jan 5, 2022

Conversation

ohad
Copy link

@ohad ohad commented Dec 8, 2021

Adds minor protocol version support

See idris2 PR#2171's new spec for Bounds

(wait until we merge #2171 before merging.)

@ohad ohad marked this pull request as ready for review December 10, 2021 11:45
@jfdm
Copy link
Contributor

jfdm commented Dec 22, 2021

@ohad Thanks for these updates. They are very much appreciated. Looking at the error, it is something I have seen before, and my fix was to drop the older versions of Emacs tested...I am, however, concerned about dropping more versions. In the past there was a soft rule that we tested against the earliest known Emacs released in Debian Stable/Ubuntu LTS. I have seen this issue discussed elsewhere which may require us to look at how we setup the emacs for testing.

@jfdm
Copy link
Contributor

jfdm commented Jan 5, 2022

@ohad I have had a look at the issue with emacs, batching, and CIs in the mentioned issue. I think the issue is that, in Emacs, we need to call initialise before we refresh the package contents. I have drafted #548 which might help your issue. If not we can investigate further.

@jfdm
Copy link
Contributor

jfdm commented Jan 5, 2022

So far so good... the Idris2 tests have completed on time, just waiting for Idris1 one's to complete. Hopefully, this will work. Once the tests have passed we can merge.

@jfdm
Copy link
Contributor

jfdm commented Jan 5, 2022

Well that was a simple fix. Apologies that this too soo long to address, for something so simple.

I have merge this.

Thanks, as always, for the contributions.

@jfdm jfdm merged commit edc2f60 into idris-hackers:main Jan 5, 2022
@ohad
Copy link
Author

ohad commented Jan 5, 2022

Thanks! Don't worry about it, I don't think it was blocking anyone (since they could have used the PR in the meanwhile).

Thanks for the fix!!

@gallais
Copy link
Contributor

gallais commented Jan 5, 2022

Ah nice. I was getting really puzzling CI errors on the idris(2)-mode merges so hopefully
that may fix that too.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants