Semantic token "property"

Stream: lean4

[Mario Carneiro]

I just noticed that the semantic highlighting support in lean 4 has three categories: keyword, variable and property. I have definitely seen keyword (tactics for example) and variable (local variables), but property (mainly .foo dot notation functions) seems to be colored the same as variable in all the default themes meaning that most lean code is a sea of red. Any thoughts about changing the textmate scope from variable.other.property (which most themes highlight the same as variable.other or variable) to something else?

[Max Nowak]

You can set a semantic color scheme in your VSCode settings.json, by adding the following:

    "editor.semanticTokenColorCustomizations": {
        "enabled": true,
        "rules": {
            "property": "#a28cb1"
        }
    },

No clue about textmate grammers. I only noticed your question because I was searching what exactly in the VSCode Lean extension actually semantically highlights stuff :D

[Leonardo de Moura]

You can also have color theme specific customizations. Here is the setting I use:

    "workbench.colorTheme": "Solarized Light",
    "editor.semanticHighlighting.enabled": true,
    "workbench.colorCustomizations": {
      "[Solarized Light]": {"editor.selectionHighlightBackground": "#e9dcc5"}
    },
    "editor.semanticTokenColorCustomizations": {
      "[Solarized Light]": {"rules": {"function": "#c1892f"}}
    },