Zulip Chat Archive

Stream: general

Topic: VS Code red thing

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?

Mario Carneiro (May 31 2019 at 18:57):

can't reproduce

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.

Kevin Buzzard (May 31 2019 at 19:26):

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

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.

Bryan Gin-ge Chen (May 31 2019 at 19:27):

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

Kevin Buzzard (May 31 2019 at 19:27):

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

Bryan Gin-ge Chen (May 31 2019 at 19:27):

Got it. :smile:

Last updated: Dec 20 2023 at 11:08 UTC