Zulip Chat Archive

Stream: general

Topic: Double line comments?


view this post on Zulip Mario Carneiro (Oct 08 2020 at 22:35):

I just noticed some peculiar syntax highlighting in vscode:

--- comment
def foo :  := 1
#check foo

Note the three dashes. Here not just the comment line but also def foo : ℕ := 1 appear commented out, but lean (and reasonable readers) do not agree, the def foo line is not commented out.

view this post on Zulip Reid Barton (Oct 08 2020 at 22:36):

I think --- is a single-line docstring comment

view this post on Zulip Reid Barton (Oct 08 2020 at 22:36):

not that this explains vscode's behavior

view this post on Zulip Mario Carneiro (Oct 08 2020 at 22:37):

--- comment
  all

  these
  lines
  are

gray
not gray

view this post on Zulip Reid Barton (Oct 08 2020 at 22:37):

hmm it doesn't actually seem to behave like one, though

view this post on Zulip Reid Barton (Oct 08 2020 at 22:38):

don't know where I got that idea then

view this post on Zulip Kevin Lacker (Oct 08 2020 at 23:17):

the highlighting of --- lines works fine in emacs lean-mode fwiw

view this post on Zulip Mario Carneiro (Oct 08 2020 at 23:18):

I assume it's something particular to vscode's syntax highlighter. Clearly zulip's highlighter is also fine

view this post on Zulip Gabriel Ebner (Oct 09 2020 at 08:03):

This is an unintended interaction between the markdown and lean highlighting.

--- This is a single-item bullet-point list.

Last updated: May 08 2021 at 04:14 UTC