Syntax highlightling

Stream: lean4

[Justus Springer]

This an example from Mathlib.Tactic.Basic in the Mathlib4 repo. VsCode seems to highlight all user-defined macros in blue, which is a little too much blue in my taste. Is this customizable?

syntax.png

[Patrick Massot]

I'm not too worried. This proof is extremely unusual in having only tactic names and no term. It clearly should be only one line: tauto so I would rather work on porting tauto instead of syntax highlighting.

[Justus Springer]

You're right of course. Independent from the example, I'm interested if there's a way to customize syntax highlighting. In the paper Beyond Notations, it's even mentioned that syntax and macro_rules were separated to allow a well-structured syntax tree pre-expansion, as to implement source code tooling such as auto-completion (and I believe syntax highlighting also falls into that category).

[Justus Springer]

So I was wondering more generally how to hack VsCode and where that's implemented :)

[Patrick Massot]

I think they're not yet at this stage of syntax highlighting but it's on the roadmap.

[Chris B]

This would probably be done with semantic highlighting which is part of the LSP protocol. It would be a change to the Lean language server rather than a per-editor/extension change. Sebastian mentioned semantic highlighting on Twitter once, but I'm not sure how much they've actually done with it yet.

[Sebastian Ullrich]

Highlighting user-declared (tactic) keywords already is semantic highlighting. We currently do context-sensitive highlighting only for identifiers where we differentiate between local and global references, but we could do something similar to tag tactic names with a custom token type.

[Justus Springer]

Thanks for the info!