Zulip Chat Archive

Stream: lean4

Topic: Syntax highlightling


Justus Springer (Aug 31 2021 at 07:31):

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 (Aug 31 2021 at 07:33):

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 (Aug 31 2021 at 07:40):

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 (Aug 31 2021 at 07:41):

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

Patrick Massot (Aug 31 2021 at 08:02):

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

Chris B (Aug 31 2021 at 08:21):

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 (Aug 31 2021 at 08:30):

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 (Aug 31 2021 at 09:03):

Thanks for the info!


Last updated: Dec 20 2023 at 11:08 UTC