Zulip Chat Archive

Stream: mathlib4

Topic: comment highlighting in Algebra.HierarchyDesign

Kevin Buzzard (Jul 20 2023 at 08:09):

At the top of this mathlib file I get headings (stuff starting with #) in comments in blue

Screenshot-from-2023-07-20-09-08-44.png

but later on down the file this stops working and everything is in green, even lines starting with ##.

Screenshot-from-2023-07-20-09-09-17.png

Is it like that for everyone?

Scott Morrison (Jul 20 2023 at 08:12):

Same for me

Scott Morrison (Jul 20 2023 at 08:12):

It seems if you unindent the code block immediately above ## Subobjects then that heading is blue again.

Eric Wieser (Jul 20 2023 at 08:15):

That looks worse in the html though

Eric Wieser (Jul 20 2023 at 08:16):

So probably we should fix the highlighter

Mario Carneiro (Jul 20 2023 at 08:16):

It looks like the nested comment in the code block is the source of the issue

Kevin Buzzard (Jul 20 2023 at 08:17):

-- colours refer to VS Code

/-!
# I am in blue!

* a bullet point
  ```
  /- a comment in indented quoted code -/
  ```

# I am now in green!
-/

Mario Carneiro (Jul 20 2023 at 08:17):

presumably a regex found the end of the comment

Eric Wieser (Jul 20 2023 at 08:17):

Does using ```lean instead of ``` to open the code blocks make any difference?

Mario Carneiro (Jul 20 2023 at 08:18):

no

Last updated: Dec 20 2023 at 11:08 UTC