vscode syntax highlighting

Stream: general

[Gabriel Ebner]

I would like to use this occasion to remind you that bug reports regarding the syntax highlighting in the vscode extension are always welcome.

[Patrick Massot]

Which occasion?

[Patrick Massot]

Rocky pasting screen-shots instead of words?

[Patrick Massot]

Oh no, I see https://github.com/leanprover/vscode-lean/commits/v0.15.1

[Bryan Gin-ge Chen]

I doubt this matters in practice, but it may be worth noting that the change to syntaxes/lean.json is only compatible with an unreleased version of 3.5c (one that includes this PR). Current versions of Lean don't allow docstrings to contain nested block comments, so the highlighting will be off.

[Gabriel Ebner]

Oh, there are more changes. :slight_smile:

[Jasmin Blanchette]

I'm probably not using the latest version, but for me "export" is not displayed in blue, unlike the other keywords.

[Chris B]

Not a bug, but is there a way to get info in the Lean Messages window to use the highlighting/bracket colorization that's specified for "normal" windows?

[Chris B]

Also is there anything written about how to use an external pretty printer not written in JS/TS with the vscode extension?

[Chris B]

Thanks for all the hard work btw.

[Gabriel Ebner]

@Jasmin Blanchette Fixed.

[Gabriel Ebner]

@Chris B If you're thinking of the bracket pair colorizer extension, that one only works in text editors and not in the HTML view. It does the bracket highlighting by adding syntax highlighting, so it doesn't work in the HTML view we use for the info view. We could of course implement this (and/or bracket matching) ourselves, but I think it would be quite a bit of work.

I'm not sure what you mean by "external pretty printers".

[Chris B]

Something like Trepplein's pretty printer. After looking around I think I might be dragging you into the weeds of lean-client-js or LSP or something so I'll do some more reading.