You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I'm one of those weird people using a light theme and with this extension the hyperlinks in goals show up as white text on a light grey background:
I've tried enabling and disabling the option to use highlighting, but that doesn't seem to change anything.
I observe a similar behavior with any of the standard light themes. The normal text changes between black and white, but the links always stay pure white.
The issue seems to be that this extension is using the --vscode-button-foreground property which stays completely white even in most light themes, because it expects to be inside a button with a dark background.
An easy way to fix it would be to treat holes and links the same and give them both the --vscode-textLink-foreground color, but I don't know if that is acceptable.
In the meantime I can work around this issue by changing the button colors in my settings:
I'm one of those weird people using a light theme and with this extension the hyperlinks in goals show up as white text on a light grey background:
I've tried enabling and disabling the option to use highlighting, but that doesn't seem to change anything.
I observe a similar behavior with any of the standard light themes. The normal text changes between black and white, but the links always stay pure white.
I am using vscodium with this full version info:
And version 0.4.7 of the agda-mode plugin.
The text was updated successfully, but these errors were encountered: