Zulip Chat Archive

Stream: general

Topic: vscode syntax highlighting

Gabriel Ebner (Feb 18 2020 at 19:17):

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 (Feb 18 2020 at 19:22):

Which occasion?

Patrick Massot (Feb 18 2020 at 19:23):

Rocky pasting screen-shots instead of words?

Patrick Massot (Feb 18 2020 at 19:25):

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

Bryan Gin-ge Chen (Feb 18 2020 at 19:31):

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 (Feb 18 2020 at 19:33):

Oh, there are more changes. :slight_smile:

Jasmin Blanchette (Feb 18 2020 at 22:27):

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

Chris B (Feb 19 2020 at 01:28):

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 (Feb 19 2020 at 01:30):

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

Chris B (Feb 19 2020 at 01:30):

Thanks for all the hard work btw.

Gabriel Ebner (Feb 19 2020 at 09:26):

@Jasmin Blanchette Fixed.

Gabriel Ebner (Feb 19 2020 at 09:30):

@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 (Feb 20 2020 at 07:10):

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.

Last updated: Aug 03 2023 at 10:10 UTC