Thank you, but I'm not sure what point you are making. The best way forward might be for you to file a pull request that fixes what you see to be the problem. Go well, – P

---

From: adql @.***>

Sent: 02 May 2024 09:58

To: plfa/plfa.github.io @.***>

Cc: Subscribed @.***>

Subject: [plfa/plfa.github.io] a:visited in code blocks messes up highlighting (Issue #989)

This email was sent to you by someone outside the University.

You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

The css has a general a:visited defined to a tint of blue, which applies to code blocks and thus changes highlighting:

code_block.png (view on web)https://github.com/plfa/plfa.github.io/assets/6893125/eedebf8f-88b4-46cf-986d-02343903f597

Here to, from, Set and extensionality have been visited. This is less critical for function and type names but, as can be seen, changes the color for record fields (and would do for the refl type constructor as well) significantly.

—

Reply to this email directly, view it on GitHub#989, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABFJ7MT7G2Y67DSAHMQP6MTZAH53XAVCNFSM6AAAAABHDJWXBWVHI2DSMVQWIX3LMV43ASLTON2WKOZSGI3TIOJXGE2TKMI.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

@wadler The issue is that clicking a definition for more info and then coming back messes up syntax highlighting.

The css has a general a:visited defined to a tint of blue, which applies to code blocks and thus changes highlighting:

Here to, from, Set and extensionality have been visited. This is less critical for function and type names but, as can be seen, changes the color for record fields (and would do for the refl type constructor as well) significantly.

I believe we use variants of Agda's CSS file.

Rather than changing the a:visited property to not capture highlighted Agda, it may be better to escalate this issue to the Agda repository and suggest changinh the Agda.css file that ships with Agda to override the colour for links with a:visited so that this becomes the default behavior across the board?

Seems like this wouldn't just be a PLFA issue.

Yes, that's right. Clicking the definitions changes the highlighting, which then remains wrong until the browser forgets the visited target, whenever that may be.

Agda.css doesn't contain any rules for a:visited, neither enabling or disabling. So it essentially reflects the style where it's embedded. I suppose escalating makes sense for a general solution.

As for PLFA itself, it seems like the "blame" is on $link-visited-color, which is defined in the various scss files in web/sass/theme/skins and applied in web/sass/theme/_base.scss#L133.

Yes, that's right. Clicking the definitions changes the highlighting, which then remains wrong until the browser forgets the visited target, whenever that may be.

Agda.css doesn't contain any rules for a:visited, neither enabling or disabling. So it essentially reflects the style where it's embedded. I suppose escalating makes sense for a general solution.

As for PLFA itself, it seems like the "blame" is on $link-visited-color, which is defined in the various scss files in web/sass/theme/skins and applied in web/sass/theme/_base.scss#L133.

No, I'm suggesting adding rules for a:visited to Agda.css that override any other highlighting to preserve consistent highlighting regardless of what other CSS is added.

I agree, my last paragraph was only for context.

I believe this is not an issue upstream in Agda after all, but rather a too low specificity of the selectors in PLFA's agda{-dark}.scss files. Check out Agda's original agda.css, where all selectors for highlighted definitions are under an .Agda parent. This is for some reason absent in PLFA's agda.scss, which causes a generic a:visited to have a higher specificity.