Manual syntax highlighting in VS Code

Stream: general

[Ioannis Konstantoulas]

The Lean 4 manual (https://leanprover.github.io/lean4/doc/faq.html) has excellent syntax highlighting for Lean; but the standard color scheme in VS Code (light modern) does not include as many variations as the text in the manual; how can I get the color scheme and highlighting details the manual uses into VS Code?

Thank you for your time!

[Patrick Massot]

It probably means you need to enable semantic syntax highlighting.

[Patrick Massot]

Open VSCode settings and search for semantic syntax highlighting.

[Scott Morrison]

More specifically, it sounds like something is wrong with your system, and the default installation instructions result in VS Code correctly syntax highlighting Lean code.

Perhaps you could show us a screen shot of your VS Code window, and/or tell us which installation instructions you used?

[Ioannis Konstantoulas]

vs_code_colors.png

Here is what my editor looks like.

[Ioannis Konstantoulas]

I do not see any settings for semantic syntax highlighting :( Searching produces no results in the editor.

[Julian Berman]

What version of VSCode are you using?

[Ioannis Konstantoulas]

Version: 1.79.2
Commit: 695af097c7bd098fbf017ce3ac85e09bbc5dda06
Date: 2023-06-17T15:54:35.168Z
Electron: 22.3.15
Chromium: 108.0.5359.215
Node.js: 16.17.1
V8: 10.8.168.25-electron.0
OS: Linux x64 6.4.1-arch2-1

[Patrick Massot]

semantic.gif

[Max Nowak 🐉]

You might have to customize the semantic token colors in your settings.json

[Max Nowak 🐉]

There’s a vscode command to show (semantic and syntactic) token types and what colors they cause. Then position your cursor over some text and you’ll see which (if any) semantic token kinda you have. For example, variables (let, params) the “variable” semantic token modifier. It should show up.

[Eric Wieser]

Does the lean manual really use semantic highlighting? If so, how does that work? I assume it's not just pygments or highlight.js?

[Sebastian Ullrich]

The Examples section uses LeanInk

[Ioannis Konstantoulas]

Is LeanInk a vs code color theme I can download?

[Ioannis Konstantoulas]

Also, I do have semantic highlighting on, it does not make a difference as to the colors being shown.

[Mac Malone]

@Ioannis Konstantoulas The screenshot you gave looks like proper syntax highlighting for the VS Code light theme (at least in my experience). What do you think it is missing?

[Ioannis Konstantoulas]

What I want is the color scheme that the Lean manual (and especially the book Functional Programming in Lean) uses. Is this not available for VS Code? My eyesight is quite bad, so I may be wrong, but it seemed to me the light theme highlights fewer groups than the color scheme in that book.

[Mac Malone]

Ioannis Konstantoulas said:

but it seemed to me the light theme highlights fewer groups than the color scheme in that book.

This is true. The the default VS Code light scheme is not very colorful. The book color scheme is much more vibrant. However, I am not sure if the book color scheme is available as a VS Code theme. This could be a good question for Sebastian.

@Sebastian Ullrich: do you happen to know if there is VS Code theme that parallels the book's color scheme or what modifications could be to approximate it?

[Sebastian Ullrich]

I don't know, it's just the standard mdBook highlighting outside of the LeanInk part

[Max Nowak 🐉]

You can customize the token colors in your vscode settings and pick a more vibrant color

[Ioannis Konstantoulas]

Thank you all!

[Sebastian Ullrich]

There is no lack of VS Code themes online, though it is not readily apparent what semantic tokens they support out of the box. Perhaps we do need our own, blessed Lean theme especially in consideration of lean4#2305