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

[vscode] Syntax highlighting for Coq 8.17-8.20 #872

Merged
merged 1 commit into from
Nov 15, 2024

Conversation

4ever2
Copy link
Contributor

@4ever2 4ever2 commented Nov 13, 2024

Add updated syntax from VSCoq Legacy and extend with new commands from Coq 8.17-8.20

@Alizter
Copy link
Collaborator

Alizter commented Nov 13, 2024

Did you cover the list in #854? I haven't been able to fully check myself yet.

@4ever2
Copy link
Contributor Author

4ever2 commented Nov 13, 2024

Not all of them are covered by this PR. Some of them seem quite hard to fix.
I don't think there is a good way to fix highlighting on Set and Add other than adding all the possible settings to the grammar.

@Alizter
Copy link
Collaborator

Alizter commented Nov 13, 2024

I guess to do Set correctly you will have to look at all the options. IIRC there should be a vernac command that prints the options table, so that might be a way to start on such a list.

I can't tell if Register some_constant. will get highlighted, I can see Register Scheme is picked up.

Also, I can't tell if Add Search Blacklist is also considered.

I've updated the list accordingly since presumably we will merge this anyway.

@4ever2
Copy link
Contributor Author

4ever2 commented Nov 13, 2024

Register some_constant. will highlight Register as a command but not some_constant as an ident.
Add Search Blacklist is not considered here.

@Alizter
Copy link
Collaborator

Alizter commented Nov 13, 2024

Register some_constant. will highlight Register as a command but not some_constant as an ident.

That's fine, as long as Register is being picked up.

@ejgallego ejgallego added this to the 0.2.3 milestone Nov 15, 2024
Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

That's fantastic, thanks so much @4ever2 !

@ejgallego ejgallego merged commit 7f470d1 into ejgallego:main Nov 15, 2024
14 checks passed
@4ever2 4ever2 deleted the syntax branch November 15, 2024 09:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants