Zulip Chat Archive

Stream: general

Topic: VS Code red thing


view this post on Zulip Kevin Buzzard (May 31 2019 at 18:52):

def ABC : add_group  := by apply_instance
#print ABC

Put the cursor on #print, revealing

def ABC : add_group ℤ :=
add_comm_group.to_add_group ℤ

in the Lean Messages window. Put your mouse on add_comm_group.to_add_group \Z and #print ABC goes red. Is that right?

view this post on Zulip Mario Carneiro (May 31 2019 at 18:57):

can't reproduce

view this post on Zulip Bryan Gin-ge Chen (May 31 2019 at 19:25):

This is the "hover decoration" feature. Hovering over messages in the infoview window causes the corresponding lines of code in the editor tab to be highlighted in red. At the moment it's not configurable, but it wouldn't be hard to expose the style as an extension setting if people wanted it.

view this post on Zulip Kevin Buzzard (May 31 2019 at 19:26):

If it's supposed to happen, that's fine.

view this post on Zulip Kevin Buzzard (May 31 2019 at 19:26):

Sometimes when things go red, it's bad, because sometimes when things go red they don't ever go un-red again, unless you put some work in.

view this post on Zulip Bryan Gin-ge Chen (May 31 2019 at 19:27):

Are you still running into issues with the decorations getting stuck?

view this post on Zulip Kevin Buzzard (May 31 2019 at 19:27):

No

view this post on Zulip Kevin Buzzard (May 31 2019 at 19:27):

But I kind of panicked when something went red anyway :-)

view this post on Zulip Bryan Gin-ge Chen (May 31 2019 at 19:27):

Got it. :smile:


Last updated: May 13 2021 at 06:15 UTC