Zulip Chat Archive

Stream: general

Topic: vscode syntax highlighting


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 18 2020 at 19:22):

Which occasion?

view this post on Zulip Patrick Massot (Feb 18 2020 at 19:23):

Rocky pasting screen-shots instead of words?

view this post on Zulip Patrick Massot (Feb 18 2020 at 19:25):

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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Feb 18 2020 at 19:33):

Oh, there are more changes. :slight_smile:

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Chris B (Feb 19 2020 at 01:30):

Thanks for all the hard work btw.

view this post on Zulip Gabriel Ebner (Feb 19 2020 at 09:26):

@Jasmin Blanchette Fixed.

view this post on Zulip 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".

view this post on Zulip 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: May 16 2021 at 05:21 UTC