search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Built-in sorts are highlighted as strings #156

Open fredrik-bakke opened 1 year ago

fredrik-bakke commented 1 year ago

Built-in sorts are highlighted as strings, but shouldn't be:

image

I suggest using a scope like support.type.sort.agda instead.

fredrik-bakke commented 1 year ago

Also, Level is not highlighted as a built-in. I don't know if this is intentional or not, but I'll record it here anyways.